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/CMakeLists.txt | |
| 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/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 |
1 files changed, 1 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 |