diff --git a/src/verification.ml b/src/verification.ml index 08552fbda7cbea1b03eb738f62606c379dde64bd..776b1ca21e97c4974e5e5f58a24db6f8e56408a2 100644 --- a/src/verification.ml +++ b/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 = diff --git a/tests/verify_json.t b/tests/verify_json.t index b625f989323acebc668bc912b62e1080cbce1655..b4493fe627f08cb4dbde43c0944a4c76346206b3 100644 --- a/tests/verify_json.t +++ b/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 ()