diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-06-23 19:07:56 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-23 22:07:56 +0000 |
| commit | c4dca0e5430e92c6a412b9fff343ff81182a0c2b (patch) | |
| tree | aeab19e4bd26175bd0c433ffa4985b11c659acbc | |
| parent | d3a82588e49606f0284f9be3732f040af841c854 (diff) | |
[regressions] Adding regression from #5371 (#6791)
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/ho/issue5371.smt2 | 7 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 53e050191..ac837b957 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -632,6 +632,7 @@ set(regress_0_tests regress0/ho/issue4477.smt2 regress0/ho/issue4990-care-graph.smt2 regress0/ho/issue5233-part1-usort-owner.smt2 + regress0/ho/issue5371.smt2 regress0/ho/issue6526.smt2 regress0/ho/ite-apply-eq.smt2 regress0/ho/lambda-equality-non-canon.smt2 diff --git a/test/regress/regress0/ho/issue5371.smt2 b/test/regress/regress0/ho/issue5371.smt2 new file mode 100644 index 000000000..740a0dc23 --- /dev/null +++ b/test/regress/regress0/ho/issue5371.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic HO_ALL) +(declare-fun a (Bool) Bool) +(assert (a false)) +(assert (a true)) +(check-sat) |