usi-verification-and-security · aehyvari · Jun 15, 2022 · Jun 27, 2022 · Jul 28, 2022 · Jul 28, 2022
diff --git a/examples/test_itp.cc b/examples/test_itp.cc
@@ -5,8 +5,7 @@ Opensmt*
 pre()
 {
     auto config = std::make_unique<SMTConfig>();
-    const char* msg;
-    config->setOption(SMTConfig::o_produce_inter, SMTOption(true), msg);
+    config->setOption(SMTConfig::o_produce_inter, SMTOption(true));
     Opensmt* osmt = new Opensmt(opensmt_logic::qf_lra, "test solver", std::move(config));
     return osmt;
 }
@@ -50,8 +49,7 @@ int main()
     {
         printf("unsat\n");
         // Set labeling function
-        const char* msg;
-        c.setOption(SMTConfig::o_itp_bool_alg, SMTOption(0), msg);
+        c.setOption(SMTConfig::o_itp_bool_alg, SMTOption(0));
 
         auto itp_context = mainSolver.getInterpolationContext();
         // Create the partitioning mask

diff --git a/examples/test_lra_itp.cc b/examples/test_lra_itp.cc
@@ -5,8 +5,7 @@ Opensmt*
 pre()
 {
     auto config = std::make_unique<SMTConfig>();
-    const char* msg;
-    config->setOption(SMTConfig::o_produce_inter, SMTOption(true), msg);
+    config->setOption(SMTConfig::o_produce_inter, SMTOption(true));
     Opensmt* osmt = new Opensmt(opensmt_logic::qf_lra, "test solver", std::move(config));
     return osmt;
 }
@@ -57,8 +56,7 @@ int main()
     {
         printf("unsat\n");
         // Set labeling function
-        const char* msg;
-        c.setOption(SMTConfig::o_itp_bool_alg, SMTOption(0), msg);
+        c.setOption(SMTConfig::o_itp_bool_alg, SMTOption(0));
         // Create the proof graph
         auto itp_context = mainSolver.getInterpolationContext();
 

diff --git a/examples/test_lra_value.cc b/examples/test_lra_value.cc
@@ -5,8 +5,7 @@ Opensmt*
 pre()
 {
     auto config = std::unique_ptr<SMTConfig>(new SMTConfig());
-    const char* msg;
-    config->setOption(SMTConfig::o_produce_inter, SMTOption(true), msg);
+    config->setOption(SMTConfig::o_produce_inter, SMTOption(true));
     Opensmt* osmt = new Opensmt(opensmt_logic::qf_lra, "test solver", std::move(config));
     return osmt;
 }
@@ -90,8 +89,7 @@ int main()
     {
         printf("unsat\n");
         // Set labeling function
-        const char* msg;
-        c.setOption(SMTConfig::o_itp_bool_alg, SMTOption(0), msg);
+        c.setOption(SMTConfig::o_itp_bool_alg, SMTOption(0));
 
         auto itp_context = mainSolver.getInterpolationContext();
         // Create the partitioning mask

diff --git a/regression/QF_BV/bar.smt2.expected.out b/regression/QF_BV/bar.smt2.expected.out
@@ -1 +1 @@
-At line 4: syntax error, unexpected TK_SYM, expecting TK_NUM or ')'
+At line 4: syntax error, unexpected TK_SYM, expecting TK_INT or ')'
diff --git a/regression/QF_LRA/clocksynchro_3clocks.worst_case_skew.induct_delta_1.smt2 b/regression/QF_LRA/clocksynchro_3clocks.worst_case_skew.induct_delta_1.smt2
@@ -1,4 +1,4 @@
-(set-option :ghost-vars 1)
+(set-option :ghost-vars true)
 (set-logic QF_LRA)
 (declare-fun v17 () Real)
 (declare-fun v23 () Real)

diff --git a/regression/generic/pre-logic.smt2.expected.out b/regression/generic/pre-logic.smt2.expected.out
@@ -6,30 +6,30 @@ success
 success
 success
 success
-success
+(error "Overflow in #xdeafbeef")
+
 success
 success
 true
 quux
 Longer story
 3
 /dev/null
-(error "No value for attr :foo-option")
-
+()
 0
-3.14159
-3736059631
+3.141593
+(error "No value for option :hex")
+
 85
-( foo string 10 4075 1.23 2 ( ( ) bar ( :keyword ) ) )
-(error "No value for attr :non-existing-option")
+(foo string #b1010 #xfeb 1.23 2 (() bar (:keyword)))
+(error "No value for option :non-existing-option")
 
 success
 success
 success
 success
 success
-(error "no value for info :foo")
-
+:foo ()
 :error-behavior commit-adultery
 :name OpenSMT
 :authors Muumi-peikko

diff --git a/regression_itp/LIA/lia_itp_split.smt2 b/regression_itp/LIA/lia_itp_split.smt2
@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (declare-fun y () Int)

diff --git a/regression_itp/LIA/lia_itp_test.smt2 b/regression_itp/LIA/lia_itp_test.smt2
@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (declare-fun y () Int)

diff --git a/regression_itp/LIA/lia_itp_test2.smt2 b/regression_itp/LIA/lia_itp_test2.smt2
@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (declare-fun y () Int)

diff --git a/regression_itp/LIA/lia_itp_test3.smt2 b/regression_itp/LIA/lia_itp_test3.smt2
@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (declare-fun y () Int)

diff --git a/regression_itp/bug_mask_ite.smt2 b/regression_itp/bug_mask_ite.smt2
@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
 
 (declare-fun x () Real)

diff --git a/regression_itp/bug_mask_ite_nested.smt2 b/regression_itp/bug_mask_ite_nested.smt2
@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
 (declare-fun |state::state.pc| () Real)
 (declare-fun |state::state.old| () Real)

diff --git a/regression_itp/dec-far1.smt2 b/regression_itp/dec-far1.smt2
@@ -1,7 +1,7 @@
 (set-option :produce-interpolants true)
-(set-option :certify-interpolants 1)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
-(set-option :interpolation-lra-algorithm 4) ; decomposed Farkas
+(set-option :interpolation-lra-algorithm 11) ; decomposed Farkas
 (declare-fun x1 () Real)
 (declare-fun x2 () Real)
 (declare-fun x3 () Real)

diff --git a/regression_itp/dec-far2.smt2 b/regression_itp/dec-far2.smt2
@@ -1,7 +1,7 @@
 (set-option :produce-interpolants true)
-(set-option :certify-interpolants 1)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
-(set-option :interpolation-lra-algorithm 4) ; decomposed Farkas
+(set-option :interpolation-lra-algorithm 11) ; decomposed Farkas
 (declare-fun x1 () Real)
 (declare-fun x2 () Real)
 (declare-fun x3 () Real)

diff --git a/regression_itp/distinct_unsat.smt2 b/regression_itp/distinct_unsat.smt2
@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
 (set-info :status unsat)
 (declare-fun a () Real)

diff --git a/regression_itp/incremental/inc_itp_theory_prop.smt2 b/regression_itp/incremental/inc_itp_theory_prop.smt2
@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LRA)
 (declare-fun x () Real)
 (push 1)

diff --git a/regression_itp/incremental/incremental_itp.smt2 b/regression_itp/incremental/incremental_itp.smt2
@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LRA)
 (declare-fun b () Bool)
 (assert (!

diff --git a/regression_itp/incremental/incremental_itp2.smt2 b/regression_itp/incremental/incremental_itp2.smt2
@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LRA)
 (declare-fun a () Real)
 (assert (!

diff --git a/regression_itp/incremental/incremental_itp3.smt2 b/regression_itp/incremental/incremental_itp3.smt2
@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LRA)
 (declare-fun a () Bool)
 (declare-fun b () Bool)

diff --git a/regression_itp/incremental/incremental_itp4.smt2 b/regression_itp/incremental/incremental_itp4.smt2
@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_UF)
 (declare-fun a () Bool)
 (declare-fun b () Bool)

diff --git a/regression_itp/incremental/incremental_itp5.smt2 b/regression_itp/incremental/incremental_itp5.smt2
@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_UF)
 (declare-fun a () Bool)
 (declare-fun b () Bool)

diff --git a/regression_itp/incremental/issue152_itp.smt2 b/regression_itp/incremental/issue152_itp.smt2
@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LRA)
 (declare-fun r11 () Real)
 (check-sat)

diff --git a/regression_itp/incremental/lia_splits.smt2 b/regression_itp/incremental/lia_splits.smt2
@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (declare-fun y () Int)

diff --git a/regression_itp/incremental/lia_splits2.smt2 b/regression_itp/incremental/lia_splits2.smt2
@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (declare-fun y () Int)

diff --git a/regression_itp/itp_bug.smt2 b/regression_itp/itp_bug.smt2
@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
 (declare-fun |state_type::state.delta| () Real)
 (declare-fun |state_type::state.v!0| () Real)

diff --git a/regression_itp/itp_bug_small.smt2 b/regression_itp/itp_bug_small.smt2
@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
 (declare-fun x () Bool)
 

diff --git a/regression_itp/part_bug.smt2 b/regression_itp/part_bug.smt2
@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
 (declare-fun |hifrog::fun_start!0#3| () Bool)
 (declare-fun |hifrog::fun_end!0#3| () Bool)

diff --git a/regression_itp/preint-options.smt2 b/regression_itp/preint-options.smt2
@@ -1,4 +1,4 @@
 (set-logic QF_LRA)
 (set-option :produce-interpolants true)
-(set-option :certify-interpolants 1)
+(set-option :certify-interpolants true)
 (check-sat)
diff --git a/regression_itp/proof_duplicate_literals.smt2 b/regression_itp/proof_duplicate_literals.smt2
@@ -1,8 +1,8 @@
-(set-option :produce-interpolants 1)
-(set-option :proof-reduce 1)
-;(set-option :proof-check 1)
+(set-option :produce-interpolants true)
+(set-option :proof-reduce true)
+;(set-option :proof-check true)
 ;(set-option :verbosity 2)
-(set-option :certify-interpolants 1)
+(set-option :certify-interpolants true)
 (set-logic QF_UF)
 (declare-fun a () Bool)
 (declare-fun b () Bool)

diff --git a/regression_itp/trivial-proof-A.smt2 b/regression_itp/trivial-proof-A.smt2
@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_UF)
 (declare-fun x () Bool)
 (assert (! false :named A))

diff --git a/regression_itp/trivial-proof-B.smt2 b/regression_itp/trivial-proof-B.smt2
@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_UF)
 (declare-fun x () Bool)
 (assert (! x :named A))

diff --git a/regression_itp/uf-itp-edge-split.smt2 b/regression_itp/uf-itp-edge-split.smt2
@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_UF)
 (declare-sort U 0)
 (declare-fun p () Bool)

diff --git a/regression_itp/uf_bug.smt2 b/regression_itp/uf_bug.smt2
@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_UF)
 (declare-sort U 0)
 (declare-fun e () U)

diff --git a/regression_itp/uf_duplicates.smt2 b/regression_itp/uf_duplicates.smt2
@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_UF)
 (declare-sort Real 0)
 (declare-fun .uf-not () Bool)

diff --git a/regression_itp/uf_itp_problem.smt2 b/regression_itp/uf_itp_problem.smt2
@@ -1,5 +1,5 @@
 (set-option :produce-interpolants true)
-(set-option :certify-interpolants 1)
+(set-option :certify-interpolants true)
 (set-logic QF_UF)
 (declare-sort Real 0)
 (declare-fun g (Real Real ) Real)

diff --git a/regression_itp/uf_local_colors_insufficient.smt2 b/regression_itp/uf_local_colors_insufficient.smt2
@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_UF)
 (declare-sort U 0)
 (declare-fun f (U U) U)

diff --git a/regression_splitting/patches/init_unsat-deep.smt2 b/regression_splitting/patches/init_unsat-deep.smt2
@@ -1,8 +1,8 @@
 0a1,7
-> (set-option :lookahead-split)
-> (set-option :lookahead-score-deep)
+> (set-option :lookahead-split true)
+> (set-option :lookahead-score-deep true)
 > (set-option :split-num 64)
-> (set-option :output-dir "splits_here")
+> (set-option :output-dir "split_and_solve_work")
 > (set-option :test_cube_and_conquer true)
 > (set-option :split-format-length "brief")
 > (set-option :split-format smt2)
diff --git a/regression_splitting/patches/init_unsat-lookahead.smt2 b/regression_splitting/patches/init_unsat-lookahead.smt2
@@ -1,7 +1,7 @@
 0a1,6
-> (set-option :lookahead-split)
+> (set-option :lookahead-split true)
 > (set-option :split-num 64)
-> (set-option :output-dir "splits_here")
+> (set-option :output-dir "split_and_solve_work")
 > (set-option :test_cube_and_conquer true)
 > (set-option :split-format-length "brief")
 > (set-option :split-format smt2)
diff --git a/regression_splitting/patches/init_unsat-scatter.smt2 b/regression_splitting/patches/init_unsat-scatter.smt2
@@ -1,4 +1,4 @@
 0a1,3
-> (set-option :scatter-split)
+> (set-option :scatter-split true)
 > (set-option :split-num 2)
 > (set-option :output-dir "split_and_solve_work")
diff --git a/regression_splitting/patches/iso_brn164-deep.smt2 b/regression_splitting/patches/iso_brn164-deep.smt2
@@ -1,10 +1,10 @@
 0a1
-> (set-option :lookahead-split)
+> (set-option :lookahead-split true)
 5a7,13
 > 
-> (set-option :lookahead-score-deep)
+> (set-option :lookahead-score-deep true)
 > (set-option :split-num 16)
-> (set-option :output-dir "splits_here")
+> (set-option :output-dir "split_and_solve_work")
 > 
 > (set-option :split-format-length "brief")
 > (set-option :split-format smt2)
diff --git a/regression_splitting/patches/iso_brn164-lookahead.smt2 b/regression_splitting/patches/iso_brn164-lookahead.smt2
@@ -1,9 +1,9 @@
 0a1
-> (set-option :lookahead-split)
+> (set-option :lookahead-split true)
 5a7,12
 > 
 > (set-option :split-num 16)
-> (set-option :output-dir "splits_here")
+> (set-option :output-dir "split_and_solve_work")
 > 
 > (set-option :split-format-length "brief")
 > (set-option :split-format smt2)
diff --git a/regression_splitting/patches/iso_brn164-scatter.smt2 b/regression_splitting/patches/iso_brn164-scatter.smt2
@@ -1,4 +1,4 @@
 0a1,3
-> (set-option :scatter-split)
+> (set-option :scatter-split true)
 > (set-option :split-num 2)
 > (set-option :output-dir "split_and_solve_work")