diff options
| author |  Valentin Wüstholz <wuestholz@gmail.com> | 2015-05-31 12:18:43 +0200 |
|---|---|---|
| committer | Valentin Wüstholz <wuestholz@gmail.com> | 2015-05-31 12:18:43 +0200 |
| commit | 39e35e01bb03719568598162d7f2142fb87ea4fe (patch) | |
| tree | d5db15fafa1efa55f33a4b7ff37e21b42426d10a /Source/Provers | |
| parent | fe892b18dbc8e0c2b5b20e509080d6e98814116c (diff) | |
Improve heuristics for diagnosing timeouts.
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 12 |
1 files changed, 6 insertions, 6 deletions
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)
{
|