Minor changes

2 files changed, 9 insertions, 0 deletions

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 30056d99..d9da29cc 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -238,6 +238,7 @@ namespace Microsoft.Boogie.Houdini {
       stats.proverTime += queryTime;

       stats.numProverQueries++;

       if (CommandLineOptions.Clo.Trace) {

+        Console.WriteLine("Outcome = " + proverOutcome);

         Console.WriteLine("Time taken = " + queryTime);

       }

 

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 9ec8b6f1..594f2509 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -1310,6 +1310,10 @@ namespace Microsoft.Boogie.SMTLib
                     break;

                   }

                 }

+                else

+                {

+                  mod = 2;

+                }

                 lastCnt = cnt;

 

                 if (0 < split0.Count)

@@ -1439,6 +1443,10 @@ namespace Microsoft.Boogie.SMTLib
         expr = VCExprGen.AndSimp(expr, lit);

       }

       SendThisVC("(assert " + VCExpr2String(expr, 1) + ")");

+      if (options.Solver == SolverKind.Z3)

+      {

+        SendThisVC("(apply (then (using-params propagate-values :max_rounds 1) simplify) :print false)");

+      }

       FlushLogFile();

       SendThisVC("(check-sat)");

       return GetResponse();