diff options
| author |  qadeer <qadeer@microsoft.com> | 2015-05-31 14:06:38 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2015-05-31 14:06:38 -0700 |
| commit | 2d2774f8aacf0e79765d6c59db4cf16c15676aef (patch) | |
| tree | ad1a34e3b7a4faa18d6c079bbe37b2cc48b39515 /Source | |
| parent | ac44a0e0ba8679be11ce0759ec58e3891a1ad318 (diff) | |
| parent | 39e35e01bb03719568598162d7f2142fb87ea4fe (diff) | |
Merge branch 'master' of https://github.com/boogie-org/boogie
Diffstat (limited to 'Source')
| -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)
{
|