Add benchmark for issue 4412 (#6287)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 58ad56276e771d3dbdc66864eaf456ea407a2f00..78576a3f85ba26bde43a50bb4d5513cb112a266b 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1760,6 +1760,7 @@ set(regress_1_tests
   regress1/quantifiers/issue4243-prereg-inc.smt2
   regress1/quantifiers/issue4290-cegqi-r.smt2
   regress1/quantifiers/issue4328-nqe.smt2
+  regress1/quantifiers/issue4412-cegqi-type.smt2 
   regress1/quantifiers/issue4433-nqe.smt2
   regress1/quantifiers/issue4620-erq-witness-unsound.smt2
   regress1/quantifiers/issue4685-wrewrite.smt2

diff --git a/test/regress/regress1/quantifiers/issue4412-cegqi-type.smt2 b/test/regress/regress1/quantifiers/issue4412-cegqi-type.smt2
new file mode 100644 (file)
index 0000000..da070d8
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue4412-cegqi-type.smt2
@@ -0,0 +1,4 @@
+(set-logic ALL)
+(set-info :status unsat)
+(assert (forall ((a Real)) (= (* (to_int (+ a 1)) (to_int a)) 1)))
+(check-sat)