mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

fix #6376

Browse source 
have solver throw an exception when user supplies a non-propositional assumption
This commit is contained in:
Nikolaj Bjorner 2022-09-30 13:03:34 -04:00
parent 6eb2d2acfa
commit ccda49bad5
1 changed files with 10 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/tactic/fd_solver/bounded_int2bv_solver.cpp
View file

@ -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);
}