diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-14 21:35:18 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-14 21:35:18 +0000 |
| commit | a648adc7767ccd720cf1684ee8adac3d03f64f53 (patch) | |
| tree | cff47c3a21e48960e5e24a0d0740bdc3c2a71d34 /src/smt | |
| parent | ae66405f6fc4af734d84b8eb2752d2706d056814 (diff) | |
add failing regression, move error up
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3da8e1b33..e3f549898 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1387,8 +1387,11 @@ void SmtEnginePrivate::processAssertions() { } if(Options::current()->repeatSimp) { + unsigned preReSimp = d_assertionsToCheck.size(); d_assertionsToCheck.swap(d_assertionsToPreprocess); simplifyAssertions(); + Assert(preReSimp == d_assertionsToCheck.size(), + "Can't add assertions here"); removeITEs(); } |