diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-20 17:28:52 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-20 22:28:52 +0000 |
| commit | dc23d706d8fa567d40b334dd89289595f5b0961a (patch) | |
| tree | 36b6fd938d7ef6f5d1ab9775d40033c5ff6c19fb /test/regress/regress1/ho | |
| parent | c7a319286027448d678327f3e950b2e6138a6abb (diff) | |
Add regressions for fixed issues (#7421)
Fixes #5288, fixes (the 3rd benchmark on) #5741, fixes #6184, fixes #5735, which do not trigger on master.
Diffstat (limited to 'test/regress/regress1/ho')
| -rw-r--r-- | test/regress/regress1/ho/issue5741-3.smt2 | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test/regress/regress1/ho/issue5741-3.smt2 b/test/regress/regress1/ho/issue5741-3.smt2 new file mode 100644 index 000000000..abc4b76a6 --- /dev/null +++ b/test/regress/regress1/ho/issue5741-3.smt2 @@ -0,0 +1,5 @@ +(set-logic HO_ALL) +(set-info :status sat) +(declare-fun p ((_ BitVec 17) (_ BitVec 16)) Bool) +(assert (p (_ bv0 17) ((_ sign_extend 15) (ite (p (_ bv0 17) (_ bv0 16)) (_ bv1 1) (_ bv0 1))))) +(check-sat) |