Merge pull request #8619 from peterschrammel/ps/fix-refine-arithmetic-simplifier

tautschnig · web-flow · commit 10a14c90fd98 · 2025-04-08T10:14:20.000+02:00
Refine-arithmetic supports simplifier
diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
@@ -204,7 +204,6 @@ 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-arithmetic") ||
                              options.get_bool_option("refine-strings");
 
   if(options.is_set("sat-solver"))

Original file line number	Diff line number	Diff line change
`@@ -204,7 +204,6 @@ get_sat_solver(message_handlert &message_handler, const optionst &options)`
`204`	`204`	`{`
`205`	`205`	`const bool no_simplifier = options.get_bool_option("beautify") \|\|`
`206`	`206`	`!options.get_bool_option("sat-preprocessor") \|\|`
`207`		`- options.get_bool_option("refine-arithmetic") \|\|`
`208`	`207`	`options.get_bool_option("refine-strings");`
`209`	`208`
`210`	`209`	`if(options.is_set("sat-solver"))`