1 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/regress1/fmf/fmf-bound-2dim.smt2 b/test/regress/regress1/fmf/fmf-bound-2dim.smt2
new file mode 100644
index 000000000..5f5c22770
--- /dev/null
+++ b/test/regress/regress1/fmf/fmf-bound-2dim.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun P (Int Int) Bool)
+
+(declare-fun a () Int)
+(assert (> a 10))
+
+(assert (forall ((x Int) (y Int))
+(=> (and (<= a x) (<= x (+ a 5)) (<= 14 y) (<= y (+ 7 x)))
+(P x y))))
+(assert (not (P 15 4)))
+
+(check-sat)