Improve Counterexamples

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

@@ -129,7 +129,7 @@ public String getSnippet() {
 
                         // line number padding + pipe + column offset
                         String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET
-                            + " ".repeat(visualColStart - 1);
+                                + " ".repeat(visualColStart - 1);
                         String markers = accentColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1));
                         sb.append(indent).append(markers);
 

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

@@ -27,20 +27,22 @@ public RefinementError(SourcePosition position, ValDerivationNode expected, ValD
 
     @Override
     public String getDetails() {
-        return "Counterexample: " + getCounterExampleString();
+        String counterexampleString = getCounterExampleString();
+        if (counterexampleString == null)
+            return "";
+        return "Counterexample: " + counterexampleString;
     }
 
     public String getCounterExampleString() {
         if (counterexample == null || counterexample.assignments().isEmpty())
-            return "";
+            return null;
 
-        // filter fresh variables and join assignements with &&
-        String counterexampleExp = counterexample.assignments().stream().filter(a -> !a.startsWith("#fresh_"))
-                .reduce((a, b) -> a + " && " + b).orElse("");
+        // join assignements with &&
+        String counterexampleExp = String.join(" && ", counterexample.assignments());
 
         // check if counterexample is trivial (same as the found value)
         if (counterexampleExp.equals(found.getValue().toString()))
-            return "";
+            return null;
 
         return counterexampleExp;
     }

liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java

@@ -18,8 +18,10 @@
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.HashMap;
+import java.util.HashSet;
 import java.util.List;
 import java.util.Map;
+import java.util.Set;
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.errors.LJError;
@@ -40,13 +42,16 @@ public class TranslatorToZ3 implements AutoCloseable {
     private final Map<String, FuncDecl<?>> funcTranslation = new HashMap<>();
     private final Map<String, Expr<?>> funcAppTranslation = new HashMap<>();
     private final Map<Expr<?>, String> exprToNameTranslation = new HashMap<>();
+    private final Set<String> instanceVariableRefinements;
 
-    public TranslatorToZ3(liquidjava.processor.context.Context c) {
-        TranslatorContextToZ3.translateVariables(z3, c.getContext(), varTranslation);
-        TranslatorContextToZ3.storeVariablesSubtypes(z3, c.getAllVariablesWithSupertypes(), varSuperTypes);
-        TranslatorContextToZ3.addAliases(c.getAliases(), aliasTranslation);
-        TranslatorContextToZ3.addGhostFunctions(z3, c.getGhosts(), funcTranslation);
-        TranslatorContextToZ3.addGhostStates(z3, c.getGhostStates(), funcTranslation);
+    public TranslatorToZ3(liquidjava.processor.context.Context context) {
+        TranslatorContextToZ3.translateVariables(z3, context.getContext(), varTranslation);
+        TranslatorContextToZ3.storeVariablesSubtypes(z3, context.getAllVariablesWithSupertypes(), varSuperTypes);
+        TranslatorContextToZ3.addAliases(context.getAliases(), aliasTranslation);
+        TranslatorContextToZ3.addGhostFunctions(z3, context.getGhosts(), funcTranslation);
+        TranslatorContextToZ3.addGhostStates(z3, context.getGhostStates(), funcTranslation);
+        instanceVariableRefinements = context.getCtxInstanceVars().stream().map(v -> v.getRefinement().toString())
+                .collect(Collectors.toSet());
     }
 
     @SuppressWarnings("unchecked")
@@ -66,17 +71,21 @@ public Counterexample getCounterexample(Model model) {
             if (decl.getArity() == 0) {
                 Symbol name = decl.getName();
                 Expr<?> value = model.getConstInterp(decl);
+                String assignment = name + " == " + value;
                 // Skip values of uninterpreted sorts
-                if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT)
-                    assignments.add(name + " == " + value);
+                if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT
+                        && !instanceVariableRefinements.contains(assignment))
+                    assignments.add(assignment);
             }
         }
         // Extract function application values
         for (Map.Entry<String, Expr<?>> entry : funcAppTranslation.entrySet()) {
-            String label = entry.getKey();
+            String name = entry.getKey();
             Expr<?> application = entry.getValue();
             Expr<?> value = model.eval(application, true);
-            assignments.add(label + " = " + value);
+            String assignment = name + " == " + value;
+            if (!instanceVariableRefinements.contains(assignment))
+                assignments.add(assignment);
         }
         return new Counterexample(assignments);
     }