diff options
| author |  shuvendu <unknown> | 2014-11-07 16:40:29 -0800 |
|---|---|---|
| committer | shuvendu <unknown> | 2014-11-07 16:40:29 -0800 |
| commit | 8bd30420a8c0ee31137b37e288b7ef69e181f3ab (patch) | |
| tree | 4a0988960c2a081bab9fbfcd4e9eeb7259cf5731 | |
| parent | 98c24910e7e01d7748930743548431a203e2be24 (diff) | |
re-enabling -useUnsatCoreForContractInfer
An example houdini\testUnsatCore.bpl to test out the unsatCore (Currently seems to be not working)
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 2 | ||||
| -rw-r--r-- | Test/houdini/testUnsatCore.bpl | 22 |
2 files changed, 23 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index ece49e23..fc2b25f1 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -81,7 +81,7 @@ namespace Microsoft.Boogie.SMTLib {
currentLogFile = OpenOutputFile("");
}
- if (CommandLineOptions.Clo.ContractInfer && CommandLineOptions.Clo.ExplainHoudini)
+ if (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini))
{
SendThisVC("(set-option :produce-unsat-cores true)");
this.usingUnsatCore = true;
diff --git a/Test/houdini/testUnsatCore.bpl b/Test/houdini/testUnsatCore.bpl new file mode 100644 index 00000000..4b9fb33b --- /dev/null +++ b/Test/houdini/testUnsatCore.bpl @@ -0,0 +1,22 @@ +// RUN: %boogie -noinfer -contractInfer -printAssignment -useUnsatCoreForContractInfer -Trace "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var g: bool;
+
+procedure foo(x:int, y:int, z:int)
+//requires
+requires br0 ==> x == 1;
+requires br1 ==> y == 1;
+requires br2 ==> z == 1;
+//ensures
+ensures be0 ==> x == 1;
+{
+
+}
+
+
+const {:existential true} br0: bool;
+const {:existential true} br1: bool;
+const {:existential true} br2: bool;
+const {:existential true} be0: bool;
+
+
|