diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-15 17:57:00 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-15 22:57:00 +0000 |
commit | 82a71608588e2cbf7ef581940abccb2f9632eef4 (patch) | |
tree | e2595a14d490d453ade5fb15bb1d4f597b720de4 /test/regress/regress1/nl | |
parent | 7649c3ba5d8df6665ff2ac18cb5df5a8dbfcd4a2 (diff) |
Add more regressions for fixed issues (#7382)
Fixes #6535, Fixes #6475, Fixes #5660, Fixes #6607, Fixes #6638, Fixes #6642, Fixes #6775.
Diffstat (limited to 'test/regress/regress1/nl')
-rw-r--r-- | test/regress/regress1/nl/issue5660-mb-success.smt2 | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test/regress/regress1/nl/issue5660-mb-success.smt2 b/test/regress/regress1/nl/issue5660-mb-success.smt2 new file mode 100644 index 000000000..6284b0580 --- /dev/null +++ b/test/regress/regress1/nl/issue5660-mb-success.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_AUFNRA) +(set-info :status sat) +(declare-fun r2 () Real) +(declare-fun r9 () Real) +(declare-fun r13 () Real) +(declare-fun ufrb5 (Real Real Real Real Real) Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun arr0 () (Array Bool Real)) +(declare-fun arr1 () (Array Bool (Array Bool Real))) +(declare-fun v5 () Bool) +(declare-fun v7 () Bool) +(declare-fun v8 () Bool) +(declare-fun v71 () Bool) +(declare-fun v81 () Bool) +(declare-fun v161 () Bool) +(assert (or v161 (and v3 (not v7)))) +(assert (or v8 (distinct v7 (and v7 v81) (ufrb5 0.0 1.0 0.0 1.0 (/ r13 r9))))) +(assert (or v161 (distinct v71 v8 (= v4 v81)))) +(assert (or v81 (= arr0 (store (select (store arr1 (xor v81 (and (= r2 1.0) (= r13 1))) arr0) v7) v81 (select (store arr0 v5 1.0) false))))) +(check-sat) |