mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Fix binding handling for quantifier free lemmas

Browse source
This commit is contained in:
Arie Gurfinkel 2017-12-26 16:48:37 -05:00
parent a8318b8822
commit ecf9c629b0
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1307,6 +1307,8 @@ bool lemma::has_binding(app_ref_vector const &binding) {
SASSERT(binding.size() == num_decls);
if (num_decls == 0) return true;
for (unsigned off = 0, sz = m_bindings.size(); off < sz; off += num_decls) {
unsigned i = 0;
for (; i < num_decls; ++i) {