diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-07 16:12:47 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-07 16:12:47 -0600 |
commit | bbca987e023b2dbf386a62731b94e41c06f32526 (patch) | |
tree | a2e617e4f4f76a97cec1a312902aa8d075eb4d36 /test/regress | |
parent | e7caa82b1def3cab78a95b38841242264124efe7 (diff) |
Fix and reenable fact vs lemma optimization in datatypes (#5614)
This corrects an issue where terms internal to datatypes were not getting properly registered e.g. as part of the indices that determine the care graph, due to a context-independent cache being used (when a SAT-context-dependent one was required).
This reenables the fact vs lemma optimization in datatypes, as it is conjectured to be correct.
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/dt-tc-opt-small.smt2 | 16 |
2 files changed, 17 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d0e28f9e5..55fe30b14 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1589,6 +1589,7 @@ set(regress_1_tests regress1/quantifiers/cdt-0208-to.smt2 regress1/quantifiers/const.cvc regress1/quantifiers/constfunc.cvc + regress1/quantifiers/dt-tc-opt-small.smt2 regress1/quantifiers/dump-inst-i.smt2 regress1/quantifiers/dump-inst-proof.smt2 regress1/quantifiers/dump-inst.smt2 diff --git a/test/regress/regress1/quantifiers/dt-tc-opt-small.smt2 b/test/regress/regress1/quantifiers/dt-tc-opt-small.smt2 new file mode 100644 index 000000000..6cf81e80a --- /dev/null +++ b/test/regress/regress1/quantifiers/dt-tc-opt-small.smt2 @@ -0,0 +1,16 @@ +; EXPECT: unknown + +; This triggered a failure related to datatypes model building (when symfpu is enabled) +(set-logic ALL) +(declare-datatypes ((V 0) (A 0)) ( + ((I (i Int)) (vec (v A))) + ((arr (l Int))))) +(declare-fun E (V V) Bool) +(declare-fun eee (A) Bool) +(declare-fun a () V) +(declare-fun aa () A) +(assert (forall ((?y1 A)) (eee ?y1))) +(assert (E a a)) +(assert (not (E (I 0) (I 0)))) +(assert (= (l aa) (i a))) +(check-sat) |