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

fix #3209

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-08 15:23:20 +01:00
parent a7b3dfb3af
commit 9b3c844c2a
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.cpp
View file

@ -2893,7 +2893,7 @@ namespace smt {
internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope
scoped_suspend_rlimit _suspend_cancel(m.limit()); scoped_suspend_rlimit _suspend_cancel(m.limit());
propagate(); propagate();
if (was_consistent && inconsistent()) { if (was_consistent && inconsistent() && !m_asserted_formulas.inconsistent()) {
// logical context became inconsistent during user PUSH // logical context became inconsistent during user PUSH
VERIFY(!resolve_conflict()); // build the proof VERIFY(!resolve_conflict()); // build the proof
} }