[tests] Added test oracles to verify-json unit test.

src/verification.ml

@@ -180,7 +180,6 @@ let combine_prover_answers answers =
     | Call_provers.Valid, r | r, Call_provers.Valid -> r
     | _ -> acc)
 
-(* TODO: does printing the task means printing the csv here?*)
 let answer_dataset limit config env prover config_prover driver dataset task =
   let dataset_predicate =
     let on_model ls =

tests/verify_json.t

@@ -14,5 +14,78 @@ Test verify-json
 
   $ PATH=$(pwd)/bin:$PATH
 
-  $ caisar verify-json config.json 2>&1 <<EOF | ./filter_tmpdir.sh
+  $ caisar verify-json config.json --verbosity=info 2>&1 <<EOF | ./filter_tmpdir.sh
+  [caisar][INFO] Specification to verify:
+  ;;; produced by PyRAT/VNN-LIB driver
+                                          ;;; produced by VNN-LIB driver
+                                          ;; X_0
+                                          (declare-const X_0 Real)
+                                          
+                                          ;; X_1
+                                          (declare-const X_1 Real)
+                                          
+                                          ;; X_2
+                                          (declare-const X_2 Real)
+                                          
+                                          ;; X_3
+                                          (declare-const X_3 Real)
+                                          
+                                          ;; X_4
+                                          (declare-const X_4 Real)
+                                          
+                                          ;; Y_0
+                                          (declare-const Y_0 Real)
+                                          
+                                          ;; Y_1
+                                          (declare-const Y_1 Real)
+                                          
+                                          ;; Y_2
+                                          (declare-const Y_2 Real)
+                                          
+                                          ;; Y_3
+                                          (declare-const Y_3 Real)
+                                          
+                                          ;; Y_4
+                                          (declare-const Y_4 Real)
+                                          
+                                          ;; axiom_ge_x0
+                                          (assert (>= X_0 0.0))
+                                          
+  ;; axiom_le_x0
+                                          (assert (<= X_0 0.299999999999999988897769753748434595763683319091796875))
+                                          
+  ;; axiom_ge_x1
+                                          (assert (>= X_1 0.6999999999999999555910790149937383830547332763671875))
+                                          
+  ;; axiom_le_x1
+                                          (assert (<= X_1 1.0))
+                                          
+  ;; axiom_ge_x2
+                                          (assert (>= X_2 0.484313724999999972720132745962473563849925994873046875))
+                                          
+  ;; axiom_le_x2
+                                          (assert (<= X_2 1.0))
+                                          
+  ;; axiom_ge_x3
+                                          (assert (>= X_3 0.0))
+                                          
+  ;; axiom_le_x3
+                                          (assert (<= X_3 0.319607843000000002575688995420932769775390625))
+                                          
+  ;; axiom_ge_x4
+                                          (assert (>= X_4 0.476470588000000028205960234117810614407062530517578125))
+                                          
+  ;; axiom_le_x4
+                                          (assert (<= X_4 1.0))
+                                          
+  ;; Goal robust_record0_y1
+                                          (assert
+                                            (or
+                                              (and (>= Y_0 Y_1))
+                                              (and (>= Y_2 Y_1))
+                                              (and (>= Y_3 Y_1))
+                                              (and (>= Y_4 Y_1))
+                                              ))
+                                          
+  [caisar][INFO] Verification results for theory 'JSON'
   [caisar] Goal property: Unknown ()