From ccda49bad5d0c033701c35c34d3d6dd79cc32dcb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Sep 2022 13:03:34 -0400 Subject: [PATCH] fix #6376 have solver throw an exception when user supplies a non-propositional assumption --- src/tactic/fd_solver/bounded_int2bv_solver.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/tactic/fd_solver/bounded_int2bv_solver.cpp b/src/tactic/fd_solver/bounded_int2bv_solver.cpp index f7974671e..ed10f7efb 100644 --- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp +++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp @@ -140,8 +140,18 @@ public: } } + void check_assumptions(unsigned num_assumptions, expr * const * assumptions) { + for (unsigned i = 0; i < num_assumptions; ++i) { + expr* arg = assumptions[i]; + m.is_not(arg, arg); + if (!is_uninterp_const(arg)) + throw default_exception("only propositional assumptions are supported for finite domains " + mk_pp(arg, m)); + } + } + lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override { flush_assertions(); + check_assumptions(num_assumptions, assumptions); return m_solver->check_sat_core(num_assumptions, assumptions); }