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

fix #4648

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-18 22:47:30 -07:00
parent ed258ca019
commit 5aaa7e0022
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/tactic/goal.cpp
View file

@ -287,7 +287,10 @@ void goal::get_formulas(expr_ref_vector & result) const {
void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) { void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
if (m_inconsistent) if (m_inconsistent)
return; return;
if (pr) { if (proofs_enabled()) {
SASSERT(pr);
if (!pr)
return;
SASSERT(f == m().get_fact(pr)); SASSERT(f == m().get_fact(pr));
expr_ref out_f(m()); expr_ref out_f(m());
proof_ref out_pr(m()); proof_ref out_pr(m());
@ -305,7 +308,6 @@ void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
} }
} }
else { else {
SASSERT(!proofs_enabled());
expr_ref fr(f, m()); expr_ref fr(f, m());
quick_process(true, fr, d); quick_process(true, fr, d);
if (!m_inconsistent) { if (!m_inconsistent) {