mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

Fix lemma::has_binding()

Browse source
This commit is contained in:
Arie Gurfinkel 2017-12-19 09:38:35 -05:00
parent ec179da0fa
commit a8318b8822
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz/spacer/spacer_context.cpp
View file

@ -1303,8 +1303,7 @@ void lemma::update_cube (pob_ref const &p, expr_ref_vector &cube) {
}
bool lemma::has_binding(app_ref_vector const &binding) {
expr *lem = get_expr();
unsigned num_decls = to_quantifier(lem)->get_num_decls();
unsigned num_decls = m_zks.size();
SASSERT(binding.size() == num_decls);