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

stash

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-04-01 07:52:55 -07:00
parent cd48a5164e
commit a2207bc35c
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/muz_qe/dl_mk_karr_invariants.cpp
View file

@ -387,6 +387,8 @@ namespace datalog {
} }
lbool is_sat = m_hb.saturate(); lbool is_sat = m_hb.saturate();
TRACE("dl_verbose", m_hb.display(tout);); TRACE("dl_verbose", m_hb.display(tout););
// TBD: actually transition function can be unsat.
// in this case the rule can be removed.
SASSERT(is_sat == l_true); SASSERT(is_sat == l_true);
dst.reset(); dst.reset();
unsigned basis_size = m_hb.get_basis_size(); unsigned basis_size = m_hb.get_basis_size();