From f2a1de1b9626dfe351dd567e106a5d4e00b19ee0 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 26 Jul 2023 18:40:45 +0100 Subject: [PATCH] --refine-arrays supports simplifier Array refinement supports using the MiniSAT simplifier. See refine_arrays.cpp/bv_refinementt::freeze_lazy_constraints. --- src/goto-checker/solver_factory.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 4e43d5185c6..2a35f5377e9 100644 --- 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"))