From c4dca0e5430e92c6a412b9fff343ff81182a0c2b Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 23 Jun 2021 19:07:56 -0300 Subject: [PATCH] [regressions] Adding regression from #5371 (#6791) --- test/regress/CMakeLists.txt | 1 + test/regress/regress0/ho/issue5371.smt2 | 7 +++++++ 2 files changed, 8 insertions(+) create mode 100644 test/regress/regress0/ho/issue5371.smt2 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) -- 2.30.2