diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-29 13:02:02 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-29 11:02:02 -0700 |
| commit | 22c36b3bceb5d1a73dc0f0355c0a01703db51acc (patch) | |
| tree | 529b8ef5a7967628742629b3322255090ed0933c /test/regress | |
| parent | 14a7be2b6fe6eb5b938927e20d275fe5c49db55e (diff) | |
Avoid circular dependencies for justifying reductions in strings extf eval (#4415)
An incorrect answer of "sat" could be found after 8 seconds on the given benchmark (with --strings-fmf) due to a circular justification for why an extended function was reduced. In particular, we ran checkExtfInference on the same term twice and then marked it as reduced since we had already seen it. This makes the code more conservative.
Notice I'm making the code doubly conservative in case there is any chance for duplication again (e.g. if ExtTheory provides duplicate terms).
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress3/strings/unsat-circ-reduce.smt2 | 13 |
2 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 656bb5880..38b741ced 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2114,6 +2114,7 @@ set(regress_3_tests regress3/sixfuncs.sy regress3/strings-any-term.sy regress3/strings/extf_d_perf.smt2 + regress3/strings/unsat-circ-reduce.smt2 ) #-----------------------------------------------------------------------------# diff --git a/test/regress/regress3/strings/unsat-circ-reduce.smt2 b/test/regress/regress3/strings/unsat-circ-reduce.smt2 new file mode 100644 index 000000000..b584c0fb1 --- /dev/null +++ b/test/regress/regress3/strings/unsat-circ-reduce.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --strings-exp --no-re-elim +; EXPECT: unsat +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun x () String) +(assert (not (= +(let ((_let_0 (re.* re.allchar ))) +(str.in_re x (re.++ re.allchar _let_0 (str.to_re "AC") _let_0 (str.to_re "CA") _let_0))) +(let ((_let_0 (+ 0 1))) (let ((_let_1 (str.indexof x "AC" _let_0))) (and (not (= _let_1 (- 1))) (not (= (str.indexof x "CA" (+ _let_1 (str.len "AC"))) (- 1)))))) +))) +(assert (<= (str.len x) 8)) +; adding --strings-fmf to command line above incorrectly said "sat" for this at ad0b69e6 +(check-sat) |