diff options
| author |  U-REDMOND\kenmcmil <kenmcmil@KENMCMIL-ASUS.redmond.corp.microsoft.com> | 2015-06-09 15:51:05 -0700 |
|---|---|---|
| committer | U-REDMOND\kenmcmil <kenmcmil@KENMCMIL-ASUS.redmond.corp.microsoft.com> | 2015-06-09 15:51:05 -0700 |
| commit | 073ddcc74e239cb9b270cc2e6db60e1daa033518 (patch) | |
| tree | 4f1115d65c9395d090c3b5eaf6439550efe2eb80 /Source/Provers | |
| parent | 8f64d5c104efe69c5d561c1b22c3e1320bba04fa (diff) | |
various changes for duality from dead codeplex repo
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 9 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 3 |
2 files changed, 10 insertions, 2 deletions
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");
|