Removed model list from being passed to VerifyImplementation

Author: zvonimir

source/ExplainError/program.cs

@@ -1333,12 +1333,11 @@ public static bool CheckIfExprFalse(Implementation impl, Expr e)
                     new List<Requires>(new Requires[] { new Requires(false, e) }), new List<IdentifierExpr>(), new List<Ensures>(new Ensures[] { new Ensures(false, Expr.False) }));
                 i.Proc = p;
                 var cexList = new List<Counterexample>();
-                var mList = new List<Model>();
                 prog.AddTopLevelDeclaration(i);
                 prog.AddTopLevelDeclaration(p);
                 prog.Resolve();
                 prog.Typecheck();
-                var result = (MyVerifyImplementation(i, ref cexList, ref mList) == VC.ConditionGeneration.Outcome.Correct);
+                var result = (MyVerifyImplementation(i, ref cexList) == VC.ConditionGeneration.Outcome.Correct);
                 prog.RemoveTopLevelDeclaration(i);
                 prog.RemoveTopLevelDeclaration(p);
                 prog.Resolve();
@@ -1350,7 +1349,7 @@ public static bool CheckIfExprFalse(Implementation impl, Expr e)
             }
             //routines for querying the verifier
             public static VC.ConditionGeneration.Outcome MyVerifyImplementation(Implementation i,
-                ref List<Counterexample> cexList, ref List<Model> mList)
+                ref List<Counterexample> cexList)
             {
                 //this creates a z3 process per vcgen
                 var checkers = new List<Checker>();
@@ -1370,7 +1369,7 @@ public static VC.ConditionGeneration.Outcome MyVerifyImplementation(Implementati
                     i.Blocks = i.OriginalBlocks;
                     i.LocVars = i.OriginalLocVars;
                 }
-                var outcome = vcgen.VerifyImplementation((Implementation)i, out cexList, out mList);
+                var outcome = vcgen.VerifyImplementation((Implementation)i, out cexList);
                 var reset = new ResetVerificationState();
                 reset.Visit(i);
                 foreach (Checker checker in checkers)
@@ -1386,8 +1385,7 @@ public static VC.ConditionGeneration.Outcome MyVerifyImplementation(Implementati
             public static VC.ConditionGeneration.Outcome MyVerifyImplementation(Implementation i)
             {
                 List<Counterexample> cexs = new List<Counterexample>();
-                List<Model> models = new List<Model>();
-                return MyVerifyImplementation(i, ref cexs, ref models);
+                return MyVerifyImplementation(i, ref cexs);
             }
             class ResetVerificationState : StandardVisitor
             {