diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-04-27 20:21:47 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-04-27 20:21:47 -0700 |
| commit | bcb6fdad0da726bbee87f1a62c921a8190a4931a (patch) | |
| tree | 408d536b36b26bd54227be5a1a3b72af7dc64ea1 /Source/BoogieDriver | |
| parent | 15aa09dfaa12ba14cdc2cd90d997479e7c01fa66 (diff) | |
unsat core for houdini
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index ed70f14e..0459c2ea 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -616,7 +616,8 @@ namespace Microsoft.Boogie { Console.WriteLine(x.Key + " = " + x.Value);
}
}
- if (CommandLineOptions.Clo.Trace) {
+ if (CommandLineOptions.Clo.Trace)
+ {
int numTrueAssigns = 0;
foreach (var x in outcome.assignment) {
if (x.Value)
@@ -625,7 +626,10 @@ namespace Microsoft.Boogie { Console.WriteLine("Number of true assignments = " + numTrueAssigns);
Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));
Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime);
+ Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime);
Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries);
+ Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries);
+ Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings);
}
foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values) {
|