diff options
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 8 | ||||
| -rw-r--r-- | Source/Houdini/Checker.cs | 3 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 2 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.csproj | 4 |
4 files changed, 11 insertions, 6 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 8262f749..5a1f8dc5 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -439,9 +439,11 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.ContractInfer) {
Houdini.Houdini houdini = new Houdini.Houdini(program, true);
Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
- Console.WriteLine("Assignment computed by Houdini:");
- foreach (var x in outcome.assignment) {
- Console.WriteLine(x.Key + " = " + x.Value);
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Assignment computed by Houdini:");
+ foreach (var x in outcome.assignment) {
+ Console.WriteLine(x.Key + " = " + x.Value);
+ }
}
errorCount = outcome.ErrorCount;
verified = outcome.Verified;
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 437dbc98..97c22cc9 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -10,6 +10,7 @@ using Microsoft.Boogie; using Microsoft.Boogie.VCExprAST;
using Microsoft.Boogie.Simplify;
using Microsoft.Boogie.Z3;
+using Microsoft.Boogie.SMTLib;
using System.Collections;
using System.IO;
using System.Threading;
@@ -50,7 +51,7 @@ namespace Microsoft.Boogie.Houdini { Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);
Hashtable/*<int, Absy!>*/ label2absy;
checker = new Checker(this, program, logFilePath, appendLogFile, impl, CommandLineOptions.Clo.ProverKillTime);
- if (!(checker.TheoremProver is Z3ProcessTheoremProver)) {
+ if (!(checker.TheoremProver is Z3ProcessTheoremProver || checker.TheoremProver is SMTLibProcessTheoremProver)) {
throw new Exception("HdnChecker only works with z3");
}
conjecture = GenerateVC(impl, null, out label2absy, checker);
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 9646ef85..1b03c507 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -754,8 +754,6 @@ namespace Microsoft.Boogie.Houdini { HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));
this.NotifyStart(program, houdiniConstants.Keys.Count);
- Console.WriteLine("Using the new houdini algorithm\n");
-
while (current.WorkList.Count > 0) {
bool exceptional = false;
System.GC.Collect();
diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj index bc7bb8c8..c4d4cb8a 100644 --- a/Source/Houdini/Houdini.csproj +++ b/Source/Houdini/Houdini.csproj @@ -110,6 +110,10 @@ <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>
<Name>Simplify</Name>
</ProjectReference>
+ <ProjectReference Include="..\Provers\SMTLib\SMTLib.csproj">
+ <Project>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</Project>
+ <Name>SMTLib</Name>
+ </ProjectReference>
<ProjectReference Include="..\Provers\Z3\Z3.csproj">
<Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>
<Name>Z3</Name>
|