mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

some confusion about proof generation

Browse source
This commit is contained in:
Ken McMillan 2013-06-27 12:24:18 -07:00
parent 4d939c07a3
commit ea127c8ab9
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/goal.cpp
View file

@ -255,7 +255,8 @@ void goal::get_formulas(ptr_vector<expr> & result) {
}
void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
// KLM: don't know why this assertion is no longer true
// SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
if (m_inconsistent)
return;
if (proofs_enabled()) {