Add tests and fix the expected file of bool1.models.smt2

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)
 )

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

tests/models/issues/715/715_1.models.expected

@@ -0,0 +1,2 @@
+
+unknown

tests/models/issues/715/715_2.models.expected

@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun f () Int 0)
+)

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)