diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-15 00:15:10 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-15 00:15:10 -0500 |
| commit | b18ebfd50bfcb3b2ec422daf5b2fd8d99ca6406a (patch) | |
| tree | 74a5814264690ecd7079743766ed6a57ee68b2fb /test | |
| parent | 0e994acb6fe6b6128d71a1f618fb6e5629118c67 (diff) | |
Do not normalize to representatives for variable equalities in conflict-based instantiation (#4280)
Conflict-based instantiation would sometimes initialize a match x -> getRepresentative(t) when a quantified formula contained x = t. This leads to issues where getRepresentative(t) is an illegal term (say, in combination with CEGQI). This makes it so the representative is accessed when necessary instead of being set as part of the match.
Fixes #4275.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 | 8 |
2 files changed, 9 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 19ccc91e4..b32f936bd 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -734,6 +734,7 @@ set(regress_0_tests regress0/quantifiers/issue2035.smt2 regress0/quantifiers/issue3655.smt2 regress0/quantifiers/issue4086-infs.smt2 + regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macros-int-real.smt2 regress0/quantifiers/macros-real-arg.smt2 diff --git a/test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 b/test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 new file mode 100644 index 000000000..51d3e89ea --- /dev/null +++ b/test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 @@ -0,0 +1,8 @@ +(set-logic UFBV) +(set-option :cbqi-all true) +(set-info :status unsat) +(declare-sort S0 0) +(declare-const S0-0 S0) +(declare-const v6 Bool) +(assert (forall ((q0 (_ BitVec 10)) (q1 S0) (q2 S0) (q3 Bool)) (xor true (and q3 q3 q3 v6 q3 q3) (= q2 q1 S0-0)))) +(check-sat) |