mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

fix #6956

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-10-19 10:34:31 -07:00
parent 37fe9cc764
commit 11ab583232
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_consequences.cpp
View file

@ -274,6 +274,12 @@ namespace smt {
expr_ref_vector& conseq, expr_ref_vector& conseq,
expr_ref_vector& unfixed) { expr_ref_vector& unfixed) {
for (expr* a : assumptions0)
if (!m.is_bool(a)) {
std::string msg = std::string("assumption ") + mk_pp(a, m) + std::string(" is not Boolean");
warning_msg(msg.c_str());
throw default_exception(msg.c_str());
}
m_antecedents.reset(); m_antecedents.reset();
m_antecedents.insert(true_literal.var(), index_set()); m_antecedents.insert(true_literal.var(), index_set());
pop_to_base_lvl(); pop_to_base_lvl();