From 68fd205cdef86b38365f39c4e9157c8964b3568a Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Fri, 12 Jun 2015 00:43:41 +0200 Subject: Fix minor issue with diagnosing timeouts. --- Source/Provers/SMTLib/ProverInterface.cs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'Source') diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index c6c04b89..7e7f0cf6 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -1317,7 +1317,9 @@ namespace Microsoft.Boogie.SMTLib } // TODO(wuestholz): Try out different ways for splitting up the work (e.g., randomly). - var split = new SortedSet(unverified.Where((val, idx) => idx < ((rem - 1) / frac + 1))); + var cnt = Math.Max(1, rem / frac); + // It seems like assertions later in the control flow have smaller indexes. + var split = new SortedSet(unverified.Where((val, idx) => (rem - idx - 1) < cnt)); Contract.Assert(0 < split.Count); var splitRes = CheckSplit(split, ref popLater, timeLimitPerAssertion, timeLimitPerAssertion, ref queries); if (splitRes == Outcome.Valid) @@ -1332,11 +1334,11 @@ namespace Microsoft.Boogie.SMTLib } else if (splitRes == Outcome.TimeOut) { - if (1 < frac && frac <= (rem / 4)) + if (2 <= frac && (4 <= (rem / frac))) { frac *= 4; } - else if (frac <= (rem / 2)) + else if (2 <= (rem / frac)) { frac *= 2; } -- cgit v1.2.3