From 073ddcc74e239cb9b270cc2e6db60e1daa033518 Mon Sep 17 00:00:00 2001 From: "U-REDMOND\\kenmcmil" Date: Tue, 9 Jun 2015 15:51:05 -0700 Subject: various changes for duality from dead codeplex repo --- Source/Provers/SMTLib/ProverInterface.cs | 9 ++++++++- Source/Provers/SMTLib/Z3.cs | 3 ++- 2 files changed, 10 insertions(+), 2 deletions(-) (limited to 'Source/Provers') diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index afb38986..c6c04b89 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -321,6 +321,8 @@ namespace Microsoft.Boogie.SMTLib SendCommon("(declare-datatypes () (" + datatypeString + "))"); } } + if (CommandLineOptions.Clo.ProverPreamble != null) + SendCommon("(include \"" + CommandLineOptions.Clo.ProverPreamble + "\")"); } if (!AxiomsAreSetup) @@ -1016,6 +1018,9 @@ namespace Microsoft.Boogie.SMTLib case "unknown": result = Outcome.Invalid; break; + case "bounded": + result = Outcome.Bounded; + break; case "error": if (resp.ArgCount > 0 && resp.Arguments[0].Name.Contains("canceled")) { @@ -1053,7 +1058,8 @@ namespace Microsoft.Boogie.SMTLib HandleProverError("Unexpected prover response: " + resp.ToString()); break; } - case Outcome.Valid: + case Outcome.Valid: + case Outcome.Bounded: { resp = Process.GetProverResponse(); if (resp.Name == "fixedpoint") @@ -1170,6 +1176,7 @@ namespace Microsoft.Boogie.SMTLib usedLogNames.Add(curFilename); } + Console.WriteLine("opening log file {0}", curFilename); return new StreamWriter(curFilename, false); } diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 250e04c9..ffa4e0cb 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -248,7 +248,8 @@ namespace Microsoft.Boogie.SMTLib // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more. // the following will make the :weight option more usable - if (!fp) options.AddWeakSmtOption("smt.QI.COST", "|(+ weight generation)|"); // TODO: this doesn't seem to work + // KLM: this QI cost function is the default + // if (!fp) options.AddWeakSmtOption("smt.QI.COST", "|(+ weight generation)|"); // TODO: this doesn't seem to work //if (options.Inspector != null) // options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100"); -- cgit v1.2.3