Rewording tests

src/lib/frontend/frontend.ml

@@ -175,7 +175,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       match SAT.get_model env with
       | None ->
         Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
-          "@[<v 0>It seems that no model has been computed so \
+          "@[<v 0>; It seems that no model has been computed so \
            far. You may need to change your model generation strategy \
            or to increase your timeouts. Returned unknown reason = %s@]" s
 

tests/models/issues/719.models.smt2 → tests/models/issues/719.models.err.smt2

@@ -16,3 +16,4 @@
     (=> (and (<= 0 p) (< p q) (<= q 10)) (<= (select a p) (select a q))))))
 (check-sat)
 (get-model)
+; (get-model) should fail because the problem is UNSAT.

tests/smtlib/testfile-get-info.dolmen.expected → tests/smtlib/testfile-get-info1.dolmen.expected

@@ -1,4 +1,3 @@
-(error "Invalid (get-info :reason-unknown)")
 
 unknown
 unsupported
@@ -10,4 +9,3 @@ unsupported
 (:name "Alt-Ergo")
 (:reason-unknown Incomplete)
 (:version dev)
-unsupported

tests/smtlib/testfile-get-info.dolmen.smt2 → tests/smtlib/testfile-get-info1.dolmen.smt2

@@ -1,17 +1,14 @@
 (set-logic ALL)
 
 (declare-const x Int)
-(declare-const y Int)
 
 (assert (= (* x x) 4))
 
-(get-info :reason-unknown)
 (check-sat)
 (get-info :all-statistics)
 (get-info :assertion-stack-levels)
 (get-info :authors)
 (get-info :error-behavior)
 (get-info :name)
 (get-info :reason-unknown)
-(get-info :version)
-(get-info :foo)
+(get-info :version)

tests/smtlib/testfile-get-info2.err.dolmen.expected

@@ -0,0 +1 @@
+(error "Invalid (get-info :reason-unknown)")

tests/smtlib/testfile-get-info2.err.dolmen.smt2

@@ -0,0 +1,8 @@
+(set-logic ALL)
+
+(declare-const x Int)
+
+(assert (= (* x x) 4))
+
+(get-info :reason-unknown)
+(check-sat)

tests/smtlib/testfile-get-info3.dolmen.expected

@@ -0,0 +1 @@
+unsupported

tests/smtlib/testfile-get-info3.dolmen.smt2

@@ -0,0 +1 @@
+(get-info :foo)