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/regress1/quantifiers/dt-tc-opt-small.smt2 | |
| 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/regress1/quantifiers/dt-tc-opt-small.smt2')
| -rw-r--r-- | test/regress/regress1/quantifiers/dt-tc-opt-small.smt2 | 16 |
1 files changed, 16 insertions, 0 deletions
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) |