From ed27ce5526bb4b42407579eb9622b9dd6251e9e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Jul 2021 11:41:55 -0700 Subject: [PATCH] fix regression in goal2sat Signed-off-by: Nikolaj Bjorner --- src/sat/tactic/goal2sat.cpp | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index bdc1b8b9e..c809ba0f8 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -304,16 +304,16 @@ struct goal2sat::imp : public sat::sat_internalizer { convert_euf(t, root, sign); return; } - else if (!is_uninterp_const(t)) { - if (!is_app(t)) { - std::ostringstream strm; - strm << mk_ismt2_pp(t, m); - throw_op_not_handled(strm.str()); - } - else - m_unhandled_funs.push_back(to_app(t)->get_decl()); - } else { + if (!is_uninterp_const(t)) { + if (!is_app(t)) { + std::ostringstream strm; + strm << mk_ismt2_pp(t, m); + throw_op_not_handled(strm.str()); + } + m_unhandled_funs.push_back(to_app(t)->get_decl()); + } + v = mk_bool_var(t); l = sat::literal(v, sign); bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);