diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-09 14:32:32 -0600 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-09 12:32:32 -0800 |
commit | 33c5eb093a7f032a7d9c9263da595eb53fdd223b (patch) | |
tree | a08a2ab95bb8e09b6be768b18b99346c48488dec /test | |
parent | b6ce0f23ce0aaa0552767e8067fe58dbceee11cb (diff) |
Fix case of uninterpreted constant instantiation in FMF (#3543)
Fixes #3537.
This benchmark triggers a potential unsoundness caused by instantiating with an uninterpreted constant (which is unsound).
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/issue3537.smt2 | 31 |
2 files changed, 32 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 787633178..edc44c3d2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1412,6 +1412,7 @@ set(regress_1_tests regress1/quantifiers/issue3316.smt2 regress1/quantifiers/issue3317.smt2 regress1/quantifiers/issue3481.smt2 + regress1/quantifiers/issue3537.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lra-vts-inf.smt2 diff --git a/test/regress/regress1/quantifiers/issue3537.smt2 b/test/regress/regress1/quantifiers/issue3537.smt2 new file mode 100644 index 000000000..0a2f3feaa --- /dev/null +++ b/test/regress/regress1/quantifiers/issue3537.smt2 @@ -0,0 +1,31 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic ALL) +(declare-datatypes ((UNIT 0)) (((Unit)) +)) +(declare-datatypes ((BOOL 0)) (((Truth) (Falsity)) +)) +(declare-sort node$type 0) +(declare-sort data$type 0) +(declare-datatypes ((cache_state$type 0)) (((invalid) (shared) (exclusive)) +)) +(declare-datatypes ((cache$type 0)) (((c_cache$type (c_state cache_state$type) (c_data data$type))) +)) +(declare-datatypes ((msg_cmd$type 0)) (((empty) (reqs) (reqe) (inv) (invack) (gnts) (gnte)) +)) +(declare-datatypes ((msg$type 0)) (((c_msg$type (m_cmd msg_cmd$type) (m_data data$type))) +)) +(declare-fun dummy () data$type) +(declare-fun memdata$1 () data$type) +(declare-fun shrset$1 () (Array node$type BOOL)) +(declare-fun recv_invack$i () node$type) +(declare-fun exgntd () BOOL) +(declare-fun chan3$1 () (Array node$type msg$type)) +(declare-fun shrset () (Array node$type BOOL)) +(declare-fun exgntd$1 () BOOL) +(declare-fun chan2 () (Array node$type msg$type)) +(declare-fun chan3 () (Array node$type msg$type)) +(declare-fun curcmd () msg_cmd$type) +(assert (distinct true (distinct true (forall ((n node$type)) (distinct false (not (= (select shrset n) Truth)) (and (= (m_cmd (select chan2 n)) empty) (= (m_cmd (select chan3 n)) empty))) ) (distinct false (= (m_cmd (select chan3 recv_invack$i)) invack) (=> (not (= curcmd empty)) (=> (= chan3$1 (store chan3 recv_invack$i (c_msg$type empty (m_data (select chan3 recv_invack$i))))) (distinct true (= shrset$1 (store shrset recv_invack$i Falsity)) (= (ite (= exgntd Truth) (ite (= false (= exgntd$1 Falsity) (=> (= memdata$1 (m_data (select chan3$1 recv_invack$i))) (exists ((n node$type)) (=> (not (= (select shrset$1 n) Truth)) (and (= (m_cmd (select chan2 n)) empty) (= (m_cmd (select chan3$1 n)) empty))) ))) Truth Falsity) (ite (forall ((n node$type)) (distinct true (not (= (select shrset$1 n) Truth)) (= true (= (m_cmd (select chan2 n)) empty) (= (m_cmd (select chan3$1 n)) empty))) ) Truth Falsity)) Truth)))))))) +(check-sat) +(exit) |