diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-23 14:28:29 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-23 14:28:29 -0500 |
| commit | b13d2f7921a65b8921ef37b38a2d4579f7c911a2 (patch) | |
| tree | df7e49fb4318fe58631ca4c4305125dd4fc32afe /test/regress/regress0 | |
| parent | c254649c8dadd9f0d94f09bf46b21f93b2c67c07 (diff) | |
Fix related to parametric sorts whose interpretation is finite due to uninterpreted sorts + FMF. Generalizes previous fix in term registration visitor.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/sc-crash-052316.smt2 | 35 |
2 files changed, 37 insertions, 1 deletions
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 575aa4159..6e1c6e918 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -55,7 +55,8 @@ TESTS = \ datatypes-ufinite-nested.smt2 \ ForElimination-scala-9.smt2 \ agree466.smt2 \ - LeftistHeap.scala-8-ncm.smt2 + LeftistHeap.scala-8-ncm.smt2 \ + sc-crash-052316.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/sc-crash-052316.smt2 b/test/regress/regress0/fmf/sc-crash-052316.smt2 new file mode 100644 index 000000000..2fc86cbed --- /dev/null +++ b/test/regress/regress0/fmf/sc-crash-052316.smt2 @@ -0,0 +1,35 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unsat + (set-logic ALL_SUPPORTED) + (set-info :status unsat) + (declare-sort g_ 0) + (declare-fun __nun_card_witness_0_ () g_) + (declare-sort f_ 0) + (declare-fun __nun_card_witness_1_ () f_) + (declare-sort e_ 0) + (declare-fun __nun_card_witness_2_ () e_) +(declare-datatypes () + ((prod1_ (Pair1_ (_select_Pair1__0 e_) (_select_Pair1__1 f_))))) + (declare-sort d_ 0) + (declare-fun __nun_card_witness_3_ () d_) + (declare-sort c_ 0) + (declare-fun __nun_card_witness_4_ () c_) + (declare-sort b_ 0) + (declare-fun __nun_card_witness_5_ () b_) + (declare-sort a_ 0) + (declare-fun __nun_card_witness_6_ () a_) +(declare-datatypes () + ((prod_ (Pair_ (_select_Pair__0 a_) (_select_Pair__1 b_))))) + (declare-fun f1_ (prod_ c_ d_ prod1_) g_) + (declare-fun g1_ (prod_) c_) + (declare-fun h_ (prod_ d_) prod1_) + (declare-fun nun_sk_0_ () prod_) +(declare-fun nun_sk_1_ (c_) d_) + (assert + (not + (exists ((v/72 c_)) + (exists ((x/73 prod1_)) + (= (f1_ nun_sk_0_ v/72 (nun_sk_1_ v/72) x/73) + (f1_ nun_sk_0_ (g1_ nun_sk_0_) (nun_sk_1_ v/72) + (h_ nun_sk_0_ (nun_sk_1_ v/72)))))))) +(check-sat) |