1 files changed, 18 insertions, 0 deletions
diff --git a/test/regress/regress1/fmf/bound-int-alt.smt2 b/test/regress/regress1/fmf/bound-int-alt.smt2
new file mode 100644
index 000000000..146487925
--- /dev/null
+++ b/test/regress/regress1/fmf/bound-int-alt.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --fmf-bound-int
+; EXPECT: sat
+(set-logic UFLIA)
+(set-info :status sat)
+(declare-sort U 0)
+(declare-sort V 0)
+(declare-fun P (U Int V Int U Int) Bool)
+
+(assert (forall ((x U) (y Int) (z V) (w Int) (v U) (d Int)) (=> (and (<= 0 d 1) (<= 2 y 6) (<= 40 w (+ 37 y))) (P x y z w v d))))
+
+(declare-fun a () U)
+(declare-fun b () V)
+
+(assert (not (P a 2 b 40 a 0)))
+(assert (not (P a 6 b 39 a 0)))
+(assert (not (P a 6 b 44 a 0)))
+
+(check-sat)