diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 4613cd089..64f1bfc9a 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -376,7 +376,7 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard, unsigned soft_sz = soft.size(); (void) soft_sz; vector clauses; - clauses.push_back(clause); + if (!clause.empty()) clauses.push_back(clause); lbool res = internal_check_assumptions(hard, soft, clauses); if (!m_use_push_bg) { m_ctx->pop(1); }