diff options
| author | Clark Barrett <barrett@cs.stanford.edu> | 2017-10-16 21:26:30 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-16 21:26:30 -0700 |
| commit | 0958ceced1107fe4be1c9f585bf5fad8fa73a7a7 (patch) | |
| tree | 3c5b003dcf3eafadbadf8f81e3b66ab814d1a2b0 /test/regress/regress0/bug1247.smt2 | |
| parent | cec475c392e7082406629a51d0da5aea7a6da151 (diff) | |
Fix for issue 1247 (#1257)
* Fix for bug 1247: in incremental mode, there was a corner case where
a skolem variable introduced during ITE removal became a solved-for
variable (part of the substitution map). But then if the same skolem
was introduced again as part of a subsequent ITE removal pass, the
substitution was not properly applied and an incorrect result was obtained.
The handling of substitutions in incremental mode is quite kludgey - I
opened an issue to revisit this.
* fixing regression
Diffstat (limited to 'test/regress/regress0/bug1247.smt2')
| -rw-r--r-- | test/regress/regress0/bug1247.smt2 | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress0/bug1247.smt2 b/test/regress/regress0/bug1247.smt2 new file mode 100644 index 000000000..e73e42fb5 --- /dev/null +++ b/test/regress/regress0/bug1247.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +(set-logic QF_ABV) +(set-info :status unsat) + +(declare-const p Bool) +(declare-const u (_ BitVec 8)) +(declare-const v (_ BitVec 8)) +(define-const t (_ BitVec 8) (ite p u v)) +(assert (= t #x01)) + +(push) +(assert (= t #x00)) +(check-sat) |