1 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/regress0/bug516.smt2 b/test/regress/regress0/bug516.smt2
new file mode 100644
index 000000000..b5f5d49eb
--- /dev/null
+++ b/test/regress/regress0/bug516.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --finite-model-find --fmf-bound-int
+; EXPECT: sat
+; EXIT: 10
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :incremental true)
+(declare-fun P (Int) Bool)
+(declare-fun ten () Int)
+
+(assert (forall ((x Int)) (=> (<= 1 x ten) (P x))))
+
+(push)
+(assert (= ten 10))
+
+(check-sat)
+(pop)