Adding new tests

src/bin/common/solving_loop.ml

@@ -314,7 +314,9 @@ let main () =
       | ".ae" -> Options.set_output_format Native
       | ".smt2" | ".psmt2" -> Options.set_output_format Smtlib2
       | s ->
-        warning "The output format %s is not supported by the Dolmen frontend." s
+        warning
+          "The output format %s is not supported by the Dolmen frontend."
+          s
   in
   (* The function In_channel.input_all is not available before OCaml 4.14. *)
   let read_all ch =
@@ -587,7 +589,7 @@ let main () =
             (* TODO: add the location of the statement. *)
             error ~default:st "No model produced."
         else
-            (* TODO: add the location of the statement. *)
+          (* TODO: add the location of the statement. *)
           error ~default:st "Model generation disabled (try --produce-models)"
 
       | {contents = `Get_info kind; _ } ->

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)