diff options
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");
|