mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

fix #3150

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-05 10:13:04 +01:00
parent 193a99da29
commit ca4a78f2ab
2 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/asserted_formulas.cpp
View file

@ -178,6 +178,8 @@ void asserted_formulas::get_assertions(ptr_vector<expr> & result) const {
} }
void asserted_formulas::push_scope() { void asserted_formulas::push_scope() {
reduce();
commit();
SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.canceled()); SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.canceled());
TRACE("asserted_formulas_scopes", tout << "before push: " << m_scopes.size() << "\n";); TRACE("asserted_formulas_scopes", tout << "before push: " << m_scopes.size() << "\n";);
m_scoped_substitution.push(); m_scoped_substitution.push();
@ -278,8 +280,6 @@ void asserted_formulas::reduce() {
flush_cache(); flush_cache();
CASSERT("well_sorted",check_well_sorted()); CASSERT("well_sorted",check_well_sorted());
// display(std::cout);
// exit(0);
} }

2
src/smt/smt_lookahead.cpp
View file

@ -82,7 +82,7 @@ namespace smt {
unsigned nf = 0, nc = 0, ns = 0, bound = 2000, n = 0; unsigned nf = 0, nc = 0, ns = 0, bound = 2000, n = 0;
for (bool_var v : vars) { for (bool_var v : vars) {
if (!ctx.bool_var2expr(v)) continue; if (!ctx.bool_var2expr(v)) continue;
literal lit(v, false); literal lit(v, false);
ctx.push_scope(); ctx.push_scope();
ctx.assign(lit, b_justification::mk_axiom(), true); ctx.assign(lit, b_justification::mk_axiom(), true);
ctx.propagate(); ctx.propagate();