Remove Previous Filtering

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java

@@ -85,20 +85,7 @@ public Map<String, CtTypeReference<?>> getContext() {
             ret.put(var.getName(), var.getType());
         return ret;
     }
-
-    public Set<String> getVariableRefinements() {
-        Set<RefinedVariable> vars = new HashSet<>();
-        vars.addAll(ctxVars.peek());
-        vars.addAll(ctxInstanceVars);
-        vars.addAll(ctxGlobalVars);
-        Set<String> refinements = new HashSet<>();
-        for (RefinedVariable var : vars) {
-            if (var.getRefinement() != null)
-                refinements.add(var.getRefinement().toString());
-        }
-        return refinements;
-    }
-
+    
     // ---------------------- Global variables ----------------------
     public void addGlobalVariableToContext(String simpleName, String location, CtTypeReference<?> type, Predicate c) {
         RefinedVariable vi = new Variable(simpleName, location, type, c);

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

@@ -38,8 +38,7 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte
                 // subRef is not a subtype of supRef
                 if (result.equals(Status.SATISFIABLE)) {
                     Model model = solver.getModel();
-                    Set<String> variableRefinements = context.getVariableRefinements();
-                    Counterexample counterexample = tz3.getCounterexample(model, variableRefinements);
+                    Counterexample counterexample = tz3.getCounterexample(model);
                     return SMTResult.error(counterexample);
                 }
             }

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

@@ -19,7 +19,6 @@
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
-import java.util.Set;
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.errors.LJError;
@@ -59,7 +58,7 @@ public Solver makeSolverForExpression(Expr<?> e) {
     /**
      * Extracts the counterexample from the Z3 model
      */
-    public Counterexample getCounterexample(Model model, Set<String> variableRefinements) {
+    public Counterexample getCounterexample(Model model) {
         List<String> assignments = new ArrayList<>();
         // Extract constant variable assignments
         for (FuncDecl<?> decl : model.getDecls()) {
@@ -68,8 +67,7 @@ public Counterexample getCounterexample(Model model, Set<String> variableRefinem
                 Expr<?> value = model.getConstInterp(decl);
                 String assignment = name + " == " + value;
                 // Skip values of uninterpreted sorts
-                if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT
-                        && !variableRefinements.contains(assignment))
+                if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT)
                     assignments.add(assignment);
             }
         }
@@ -79,8 +77,7 @@ public Counterexample getCounterexample(Model model, Set<String> variableRefinem
             Expr<?> application = entry.getValue();
             Expr<?> value = model.eval(application, true);
             String assignment = name + " == " + value;
-            if (!variableRefinements.contains(assignment))
-                assignments.add(assignment);
+            assignments.add(assignment);
         }
         return new Counterexample(assignments);
     }