diff --git a/tests/models/issues/719.models.expected b/tests/models/issues/719.models.expected
new file mode 100644
index 000000000..1b1ed6e84
--- /dev/null
+++ b/tests/models/issues/719.models.expected
@@ -0,0 +1,3 @@
+
+unsat
+(error "No model produced.")
diff --git a/tests/models/issues/719.models.smt2 b/tests/models/issues/719.models.smt2
new file mode 100644
index 000000000..d717b2e50
--- /dev/null
+++ b/tests/models/issues/719.models.smt2
@@ -0,0 +1,18 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const a (Array Int Int))
+(declare-const s Int)
+(assert (and (<= 0 s) (<= s 10)))
+(assert (forall ((k Int)) (=> (and (<= 0 k) (< k s)) (<= (select a k) (select a s)))))
+(assert (forall ((k Int)) (=> (and (< s k) (<= k 10)) (<= (select a s) (select a k)))))
+(assert (
+  forall ((p Int) (q Int))
+    (=> (and (<= 0 p) (< p q) (<= q (- s 1))) (<= (select a p) (select a q)))))
+(assert (
+  forall ((p Int) (q Int))
+    (=> (and (<= (+ s 1) p) (< p q) (<= q 10)) (<= (select a p) (select a q)))))
+(assert (not (
+  forall ((p Int) (q Int))
+    (=> (and (<= 0 p) (< p q) (<= q 10)) (<= (select a p) (select a q))))))
+(check-sat)
+(get-model)