diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-19 19:28:08 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-19 19:28:08 -0600 |
commit | c8e8acd26b4bd5c47110b9448a74a45913b5518f (patch) | |
tree | 91a27c3e9269e2ff4f852fb7b4d7475e00826ef0 /test/regress | |
parent | 3c754308f66d92cd4b03d5f159464585c315b528 (diff) |
Use arbitrary ground term assignment for sorts where isInterpretedFinite is true (#5790)
This makes a small change to our model construction to assign arbitrary values to eqc for types that are "interpreted finite", that is, have finite cardinality under the assumption that uninterpreted sorts are finite/infinite (when finite model finding is on/off). Uninterpreted sorts themselves always use the type enumerator to assign distinct values.
This fixes #5738.
This change is necessary since there was previously a mismatch between types where isFinite != isInterpretedFinite, in particular a datatype with a single constructor with a unintepreted type field as in that issue.
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2 | 16 |
2 files changed, 17 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index e2af099d7..d35758d5c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1504,6 +1504,7 @@ set(regress_1_tests regress1/fmf/issue3689.smt2 regress1/fmf/issue4068-si-qf.smt2 regress1/fmf/issue4225-univ-fun.smt2 + regress1/fmf/issue5738-dt-interp-finite.smt2 regress1/fmf/issue916-fmf-or.smt2 regress1/fmf/jasmin-cdt-crash.smt2 regress1/fmf/ko-bound-set.cvc diff --git a/test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2 b/test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2 new file mode 100644 index 000000000..50373fde4 --- /dev/null +++ b/test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2 @@ -0,0 +1,16 @@ +(set-logic UFLIA) +(set-info :status sat) +(set-option :finite-model-find true) +(declare-sort a 0) +(declare-sort b 0) +(declare-datatypes ((c 0)) (((d (m b))))) +(declare-sort d 0) +(declare-sort e 0) +(declare-datatypes ((f 0)) (((n)))) +(declare-fun o (f e d c) a) +(declare-fun g (f) e) +(declare-fun h (f d) c) +(declare-fun i () f) +(declare-fun j (e) d) +(assert (forall ((k e)) (exists ((l c)) (= (o i k (j k) l) (o i (g i) (j k) (h i (j k))))))) +(check-sat) |