Unsimplified Expression Debug Log

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java

@@ -123,6 +123,13 @@ public static void smtStart(VCImplication chain, Predicate extraPremise, Predica
         System.out.println(SMT_TAG + " " + formatConclusion(conclusion));
     }
 
+    public static void simplificationInput(Predicate predicate) {
+        if (!enabled()) {
+            return;
+        }
+        System.out.println(SMT_TAG + " unsimplified: " + predicate);
+    }
+
     private static String plainLabel(VCImplication node) {
         return node.getName() + " : " + simpleType(node.getType());
     }

liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java

@@ -6,7 +6,7 @@
 import java.util.Map;
 import java.util.stream.Collectors;
 
-import liquidjava.api.CommandLineLauncher;
+import liquidjava.diagnostics.DebugLog;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.errors.NotFoundError;
 import liquidjava.processor.context.AliasWrapper;
@@ -252,14 +252,13 @@ public Expression getExpression() {
     }
 
     public ValDerivationNode simplify(Context context) {
+        DebugLog.simplificationInput(this);
+
         // collect aliases from context
         Map<String, AliasDTO> aliases = new HashMap<>();
         for (AliasWrapper aw : context.getAliases()) {
             aliases.put(aw.getName(), aw.createAliasDTO());
         }
-        if (CommandLineLauncher.cmdArgs.debugMode) {
-            return new ValDerivationNode(exp.clone(), null);
-        }
         // simplify expression
         return ExpressionSimplifier.simplify(exp.clone(), aliases);
     }