From e95e704f362690377d851fe80bbc778877bbfc69 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 5 Apr 2021 15:25:37 -0500 Subject: [PATCH] Add benchmark for issue 4412 (#6287) --- test/regress/CMakeLists.txt | 1 + test/regress/regress1/quantifiers/issue4412-cegqi-type.smt2 | 4 ++++ 2 files changed, 5 insertions(+) create mode 100644 test/regress/regress1/quantifiers/issue4412-cegqi-type.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 58ad56276..78576a3f8 100644 --- 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 index 000000000..da070d8d6 --- /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) -- 2.30.2