Merge pull request #7828 from peterschrammel/ps/refine-arrays-with-simplifier

tautschnig · web-flow · commit 0c029ea92abd · 2023-08-01T10:58:55.000+02:00
--refine-arrays actually supports simplifier
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"))`