From d4b984fe34c2801582145507e596d6ebe35627cf Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 14 Feb 2020 15:01:55 +0000 Subject: [PATCH] Refine-arrays: work with refine-strings --- src/goto-checker/solver_factory.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 90b67d8de06..c269582c921 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -131,8 +131,12 @@ std::unique_ptr solver_factoryt::get_solver() { if(options.get_bool_option("dimacs")) return get_dimacs(); - if(options.get_bool_option("refine")) + if( + options.get_bool_option("refine") && + !options.get_bool_option("refine-strings")) + { return get_bv_refinement(); + } else if(options.get_bool_option("refine-strings")) return get_string_refinement(); if(options.get_bool_option("smt2"))