--refine-arrays supports simplifier

peterschrammel · peterschrammel · commit f2a1de1b9626 · 2023-07-26T18:40:49.000+01:00
Array refinement supports using the MiniSAT simplifier.
See refine_arrays.cpp/bv_refinementt::freeze_lazy_constraints.
diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
@@ -224,7 +224,7 @@ get_sat_solver(message_handlert &message_handler, const optionst &options)
 {
   const bool no_simplifier = options.get_bool_option("beautify") ||
                              !options.get_bool_option("sat-preprocessor") ||
-                             options.get_bool_option("refine") ||
+                             options.get_bool_option("refine-arithmetic") ||
                              options.get_bool_option("refine-strings");
 
   if(options.is_set("sat-solver"))

Original file line number	Diff line number	Diff line change
`@@ -224,7 +224,7 @@ get_sat_solver(message_handlert &message_handler, const optionst &options)`
`224`	`224`	`{`
`225`	`225`	`const bool no_simplifier = options.get_bool_option("beautify") \|\|`
`226`	`226`	`!options.get_bool_option("sat-preprocessor") \|\|`
`227`		`- options.get_bool_option("refine") \|\|`
	`227`	`+ options.get_bool_option("refine-arithmetic") \|\|`
`228`	`228`	`options.get_bool_option("refine-strings");`
`229`	`229`
`230`	`230`	`if(options.is_set("sat-solver"))`