diff --git a/tests/models/bool/bool1.models.expected b/tests/models/bool/bool1.models.expected
index d75528555..0ccd1ace6 100644
--- a/tests/models/bool/bool1.models.expected
+++ b/tests/models/bool/bool1.models.expected
@@ -7,5 +7,4 @@ unknown
 (
   (define-fun p () Bool true)
   (define-fun q () Bool true)
-  (define-fun nq () Bool true)
 )
diff --git a/tests/models/issues/715/715_1.models.ae b/tests/models/issues/715/715_1.models.ae
new file mode 100644
index 000000000..84ef6c34f
--- /dev/null
+++ b/tests/models/issues/715/715_1.models.ae
@@ -0,0 +1,6 @@
+logic f: int
+
+(* This function is user-defined and shouldn't appear in the output model. *)
+function g(x: int, y: int) : int = x + y
+
+check_sat t: f = 0
diff --git a/tests/models/issues/715/715_1.models.expected b/tests/models/issues/715/715_1.models.expected
new file mode 100644
index 000000000..a6e005255
--- /dev/null
+++ b/tests/models/issues/715/715_1.models.expected
@@ -0,0 +1,2 @@
+
+unknown
diff --git a/tests/models/issues/715/715_2.models.expected b/tests/models/issues/715/715_2.models.expected
new file mode 100644
index 000000000..966bb2f29
--- /dev/null
+++ b/tests/models/issues/715/715_2.models.expected
@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun f () Int 0)
+)
diff --git a/tests/models/issues/715/715_2.models.smt2 b/tests/models/issues/715/715_2.models.smt2
new file mode 100644
index 000000000..93a28138c
--- /dev/null
+++ b/tests/models/issues/715/715_2.models.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const f Int)
+(assert (= f 0))
+; This function is user-defined and shouldn't appear in the output model.
+(define-fun g ((x Int) (y Int)) Int (+ x y))
+(check-sat)
+(get-model)