mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Fix to cube-and-clause interface in prop_solver

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-03 09:13:38 -07:00
parent e0e435582a
commit 268274911a
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz/spacer/spacer_prop_solver.cpp
View file

@ -376,7 +376,7 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
unsigned soft_sz = soft.size(); unsigned soft_sz = soft.size();
(void) soft_sz; (void) soft_sz;
vector<expr_ref_vector> clauses; vector<expr_ref_vector> clauses;
clauses.push_back(clause); if (!clause.empty()) clauses.push_back(clause);
lbool res = internal_check_assumptions(hard, soft, clauses); lbool res = internal_check_assumptions(hard, soft, clauses);
if (!m_use_push_bg) { m_ctx->pop(1); } if (!m_use_push_bg) { m_ctx->pop(1); }