Only Get ctxVars in the Current Scope

Author: rcosta358

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

@@ -86,9 +86,9 @@ public Map<String, CtTypeReference<?>> getContext() {
         return ret;
     }
 
-    public Set<String> getAllVariableRefinements() {
+    public Set<String> getVariableRefinements() {
         Set<RefinedVariable> vars = new HashSet<>();
-        vars.addAll(getAllCtxVars());
+        vars.addAll(ctxVars.peek());
         vars.addAll(ctxInstanceVars);
         vars.addAll(ctxGlobalVars);
         Set<String> refinements = new HashSet<>();

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

@@ -38,7 +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.getAllVariableRefinements();
+                    Set<String> variableRefinements = context.getVariableRefinements();
                     Counterexample counterexample = tz3.getCounterexample(model, variableRefinements);
                     return SMTResult.error(counterexample);
                 }