Send initialisation commands to solver

thomasspriggs · thomasspriggs · commit aad1bf526ced · 2021-09-22T10:34:15.000+01:00
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -2,6 +2,7 @@
 
 #include "smt2_incremental_decision_procedure.h"
 
+#include <solvers/smt2_incremental/smt_commands.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
 #include <util/expr.h>
 #include <util/string_utils.h>
@@ -12,6 +13,9 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
     number_of_solver_calls{0},
     solver_process{split_string(solver_command, ' ', false, true)}
 {
+  send_to_solver(smt_set_option_commandt{smt_option_produce_modelst{true}});
+  send_to_solver(smt_set_logic_commandt{
+    smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}});
 }
 
 exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)

Original file line number	Diff line number	Diff line change
`@@ -2,6 +2,7 @@`
`2`	`2`
`3`	`3`	`#include "smt2_incremental_decision_procedure.h"`
`4`	`4`
	`5`	`+#include <solvers/smt2_incremental/smt_commands.h>`
`5`	`6`	`#include <solvers/smt2_incremental/smt_to_smt2_string.h>`
`6`	`7`	`#include <util/expr.h>`
`7`	`8`	`#include <util/string_utils.h>`
`@@ -12,6 +13,9 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(`
`12`	`13`	`number_of_solver_calls{0},`
`13`	`14`	`solver_process{split_string(solver_command, ' ', false, true)}`
`14`	`15`	`{`
	`16`	`+ send_to_solver(smt_set_option_commandt{smt_option_produce_modelst{true}});`
	`17`	`+ send_to_solver(smt_set_logic_commandt{`
	`18`	`+ smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}});`
`15`	`19`	`}`
`16`	`20`
`17`	`21`	`exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)`