mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

Cleanup

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-21 23:36:37 -04:00
parent 58dc5451e1
commit 7b2ca769ef
1 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/muz/spacer/spacer_proof_utils.cpp
View file

@ -94,10 +94,11 @@ namespace spacer {
family_id tid = m.mk_family_id(params[0].get_symbol()); family_id tid = m.mk_family_id(params[0].get_symbol());
SASSERT(tid != null_family_id); SASSERT(tid != null_family_id);
proof *pf = m.mk_th_lemma(tid, m.mk_false(), proof_ref pf(m);
parents.size(), parents.c_ptr(), pf = m.mk_th_lemma(tid, m.mk_false(),
v.size(), v.c_ptr()); parents.size(), parents.c_ptr(),
return proof_ref(pf, m); v.size(), v.c_ptr());
return pf;
} }
// convert assign-bounds lemma to a farkas lemma by adding missing coeff // convert assign-bounds lemma to a farkas lemma by adding missing coeff