Counterexample Debug Log

Author: rcosta358

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

@@ -9,6 +9,7 @@
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.GroupExpression;
+import liquidjava.smt.Counterexample;
 import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.reference.CtTypeReference;
@@ -130,6 +131,16 @@ public static void simplificationInput(Predicate predicate) {
         System.out.println(SMT_TAG + " unsimplified: " + predicate);
     }
 
+    public static void counterexampleAssignments(Counterexample counterexample) {
+        if (!enabled() || counterexample == null || counterexample.assignments().isEmpty()) {
+            return;
+        }
+        System.out.println(SMT_TAG + " counterexample assignments:");
+        for (var assignment : counterexample.assignments()) {
+            System.out.println(SMT_TAG + "     " + assignment.first() + " = " + assignment.second());
+        }
+    }
+
     private static String plainLabel(VCImplication node) {
         return node.getName() + " : " + simpleType(node.getType());
     }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -4,7 +4,7 @@
 import java.util.List;
 import java.util.stream.Collectors;
 
-import liquidjava.api.CommandLineLauncher;
+import liquidjava.diagnostics.DebugLog;
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
@@ -44,6 +44,8 @@ public String getCounterExampleString() {
         if (counterexample == null || counterexample.assignments().isEmpty())
             return null;
 
+        DebugLog.counterexampleAssignments(counterexample);
+
         List<String> foundVarNames = new ArrayList<>();
         found.getValue().getVariableNames(foundVarNames);
         // also keep resolved static-final constants (e.g. Integer.MAX_VALUE) referenced by either side of the
@@ -53,8 +55,8 @@ public String getCounterExampleString() {
         List<String> foundAssignments = found.getValue().getConjuncts().stream().map(Expression::toString).toList();
         String counterexampleString = counterexample.assignments().stream()
                 // only include variables that appear in the found value and are not already fixed there
-                .filter(a -> CommandLineLauncher.cmdArgs.debugMode || (foundVarNames.contains(a.first())
-                        && !foundAssignments.contains(a.first() + " == " + a.second())))
+                .filter(a -> foundVarNames.contains(a.first())
+                        && !foundAssignments.contains(a.first() + " == " + a.second()))
                 // format as "var == value"
                 .map(a -> VariableFormatter.format(a.first()) + " == " + a.second())
                 // join with "&&"