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/regress/regress0 | |
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/regress/regress0')
-rw-r--r-- | test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 | 8 |
1 files changed, 8 insertions, 0 deletions
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) |