fixed a bug where a formula was being send to CVC4 although it shouldn't normally

1 files changed, 3 insertions, 1 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 68976183..18644a6d 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -891,6 +891,8 @@ namespace Microsoft.Boogie.SMTLib
         else if (resp.ArgCount != 0)

           break;

         path.Add(v);

+		if (v.Equals("0"))

+		  throw new UnexpectedProverOutputException("because of (get-value ((ControlFlow " + controlFlowConstant + " " + v + ")))");

         SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " " + v + ")))");

       }

       return path.ToArray();

@@ -913,7 +915,7 @@ namespace Microsoft.Boogie.SMTLib
         if (resp.Name == "model" && resp.ArgCount >= 1) {

 					modelStr = resp.Arguments[0] + "\n";

 					for (int i = 1; i < resp.ArgCount; i++) {

-						if (resp.Arguments[i].ToString().Contains("define-fun"))

+						if (resp.Arguments[i].ToString().Contains("define-fun") &&!resp.Arguments[i].ToString().Contains("not"))

 							modelStr += resp.Arguments[i] + "\n";

 					}

 					//Console.WriteLine(modelStr);