From 39e35e01bb03719568598162d7f2142fb87ea4fe Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Sun, 31 May 2015 12:18:43 +0200 Subject: Improve heuristics for diagnosing timeouts. --- Source/Provers/SMTLib/ProverInterface.cs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'Source') diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index e09eabcb..c257ea14 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -1284,14 +1284,14 @@ namespace Microsoft.Boogie.SMTLib if (lastCnt == cnt) { - if ((2 * frac) < cnt) + if (frac < (cnt / 2)) { frac *= 2; } - else if (timeLimitFactor <= 3 && 0 < timeLimit) + else if (0 < timeLimit && timeLimitFactor <= 4) { // TODO(wuestholz): Add a commandline option to control this. - timeLimitFactor++; + timeLimitFactor *= 2; } else { @@ -1309,6 +1309,7 @@ namespace Microsoft.Boogie.SMTLib else { frac = 2; + timeLimitFactor = 1; } lastCnt = cnt; @@ -1319,8 +1320,7 @@ namespace Microsoft.Boogie.SMTLib if (0 < split0.Count) { - var stl = 0 < timeLimit ? split0.Count * ((timeLimit / cnt) + 1) : timeLimit; - var result0 = CheckSplit(split0, ref popLater, timeLimitFactor * stl); + var result0 = CheckSplit(split0, ref popLater, timeLimitFactor * timeLimit); if (result0 == Outcome.Valid) { unverified.ExceptWith(split0); @@ -1334,7 +1334,7 @@ namespace Microsoft.Boogie.SMTLib if (0 < split1.Count) { - var stl = 0 < timeLimit ? split1.Count * ((timeLimit / cnt) + 1) : timeLimit; + var stl = 0 < timeLimit ? (frac - 1) * timeLimit : timeLimit; var result1 = CheckSplit(split1, ref popLater, timeLimitFactor * stl); if (result1 == Outcome.Valid) { -- cgit v1.2.3