mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Debug sanity check in spacer_context

Browse source 
Triggered by bugs in hypothesis remover

only sanitycheck lemmas in debug-mode
This commit is contained in:
Bernhard Gleiss 2017-11-27 16:46:14 +01:00 • committed by Arie Gurfinkel
parent a4e67b8bb6
commit 247c570e6b
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3133,7 +3133,12 @@ lbool context::expand_node(pob& n)
checkpoint ();
(*m_lemma_generalizers[i])(lemma);
}
DEBUG_CODE(
lemma_sanity_checker sanity_checker(*this);
sanity_checker(lemma);
);
TRACE("spacer", tout << "invariant state: "
<< (is_infty_level(lemma->level())?"(inductive)":"")
<< mk_pp(lemma->get_expr(), m) << "\n";);