Add benchmark for issue 5101 (#6301)

Fixes #5101.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 080030a7e592ae36391f1fd2e620381988d320a5..048372c69922fc702c1f38df0c7681e794c91571 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1561,6 +1561,7 @@ set(regress_1_tests
   regress1/issue3990-sort-inference.smt2
   regress1/issue4273-ext-rew-cache.smt2
   regress1/issue4335-unsat-core.smt2
+  regress1/issue5101-alira-subtypes.smt2
   regress1/issue5739-rtf-processed.smt2
   regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
   regress1/lemmas/pursuit-safety-8.smtv1.smt2

diff --git a/test/regress/regress1/issue5101-alira-subtypes.smt2 b/test/regress/regress1/issue5101-alira-subtypes.smt2
new file mode 100644 (file)
index 0000000..a48aab1
--- /dev/null
+++ b/test/regress/regress1/issue5101-alira-subtypes.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AUFLIRA)
+(set-info :status sat)
+(declare-fun _substvar_173_ () Bool)
+(declare-const v9 Bool)
+(declare-const r0 Real)
+(declare-const r7 Real)
+(declare-const r10 Real)
+(declare-const i17 Int)
+(declare-const arr (Array Real Real))
+(assert (or _substvar_173_ (> 0.0 r10 (select (store arr r0 (to_real i17)) 817949693.0))))
+(assert (or v9 (is_int r7)))
+(check-sat)