summaryrefslogtreecommitdiff
path: root/Source/Provers
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs37
1 files changed, 33 insertions, 4 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index c257ea14..e9cb9a08 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -454,7 +454,7 @@ namespace Microsoft.Boogie.SMTLib
ctx.KnownDatatypeConstructors.Clear();
ctx.parent = this;
DeclCollector.Reset();
- SendThisVC("; doing a full reset...");
+ SendThisVC("; did a full reset");
}
}
@@ -1266,11 +1266,19 @@ namespace Microsoft.Boogie.SMTLib
{
#region Run timeout diagnostics
+ if (CommandLineOptions.Clo.TraceDiagnosticsOnTimeout)
+ {
+ Console.Out.WriteLine("Starting timeout diagnostics with initial time limit {0}.", options.TimeLimit);
+ }
+
+ var start = DateTime.UtcNow;
+
SendThisVC("; begin timeout diagnostics");
var unverified = new SortedSet<int>(ctx.TimeoutDiagnosticIDToAssertion.Keys);
var lastCnt = 0;
var timeLimit = options.TimeLimit;
+ var timeLimitPerAssertion = CommandLineOptions.Clo.TimeLimitPerAssertionInMs;
var timeLimitFactor = 1;
var frac = 2;
while (true)
@@ -1320,7 +1328,9 @@ namespace Microsoft.Boogie.SMTLib
if (0 < split0.Count)
{
- var result0 = CheckSplit(split0, ref popLater, timeLimitFactor * timeLimit);
+ var tl = timeLimitFactor * timeLimit;
+ var tla = timeLimitPerAssertion * split0.Count;
+ var result0 = CheckSplit(split0, ref popLater, (0 < tla && tla < tl) ? tla : tl);
if (result0 == Outcome.Valid)
{
unverified.ExceptWith(split0);
@@ -1334,8 +1344,10 @@ namespace Microsoft.Boogie.SMTLib
if (0 < split1.Count)
{
- var stl = 0 < timeLimit ? (frac - 1) * timeLimit : timeLimit;
- var result1 = CheckSplit(split1, ref popLater, timeLimitFactor * stl);
+ var tl = 0 < timeLimit ? (frac - 1) * timeLimit : timeLimit;
+ tl = timeLimitFactor * tl;
+ var tla = timeLimitPerAssertion * split1.Count;
+ var result1 = CheckSplit(split1, ref popLater, (0 < tla && tla < tl) ? tla : tl);
if (result1 == Outcome.Valid)
{
unverified.ExceptWith(split1);
@@ -1350,6 +1362,23 @@ namespace Microsoft.Boogie.SMTLib
SendThisVC("; end timeout diagnostics");
+ var end = DateTime.UtcNow;
+
+ if (CommandLineOptions.Clo.TraceDiagnosticsOnTimeout)
+ {
+ Console.Out.WriteLine("Terminated timeout diagnostics after {0:F0} ms.", end.Subtract(start).TotalMilliseconds);
+ Console.Out.WriteLine("Outcome: {0}", result);
+ Console.Out.WriteLine("Unverified assertions: {0} (of {1})", unverified.Count, ctx.TimeoutDiagnosticIDToAssertion.Keys.Count);
+
+ string filename = "unknown";
+ var assertion = ctx.TimeoutDiagnosticIDToAssertion.Values.Select(t => t.Item1).FirstOrDefault(a => a.tok != null && a.tok != Token.NoToken && a.tok.filename != null);
+ if (assertion != null)
+ {
+ filename = assertion.tok.filename;
+ }
+ File.AppendAllText("timeouts.csv", string.Format(";{0};{1};{2:F0};{3};{4};{5}\n", filename, options.TimeLimit, end.Subtract(start).TotalMilliseconds, result, unverified.Count, ctx.TimeoutDiagnosticIDToAssertion.Keys.Count));
+ }
+
#endregion
}