From 15d853dc04138c98bf8b193842cb4033b36dedff Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 24 Jan 2023 04:15:52 -0800
Subject: [PATCH] add trail to avoid stale references in expr2var
---
src/ast/simplifiers/bound_simplifier.cpp | 4 ++++
src/ast/simplifiers/bound_simplifier.h | 3 +++
2 files changed, 7 insertions(+)
diff --git a/src/ast/simplifiers/bound_simplifier.cpp b/src/ast/simplifiers/bound_simplifier.cpp
index 89ed6da05..06302ab6f 100644
--- a/src/ast/simplifiers/bound_simplifier.cpp
+++ b/src/ast/simplifiers/bound_simplifier.cpp
@@ -208,6 +208,8 @@ void bound_simplifier::tighten_bound(dependent_expr const& de) {
assert_upper(x, n - k, true);
}
+
+
// x != k, k <= x -> k < x
if (m.is_not(f, f) && m.is_eq(f, x, y)) {
if (a.is_numeral(x))
@@ -222,6 +224,7 @@ void bound_simplifier::tighten_bound(dependent_expr const& de) {
assert_upper(x, n, true);
}
}
+
}
void bound_simplifier::assert_upper(expr* x, rational const& n, bool strict) {
@@ -449,6 +452,7 @@ void bound_simplifier::reset() {
bp.reset();
m_var2expr.reset();
m_expr2var.reset();
+ m_trail.reset();
}
#if 0
diff --git a/src/ast/simplifiers/bound_simplifier.h b/src/ast/simplifiers/bound_simplifier.h
index 6977261c5..7950f418b 100644
--- a/src/ast/simplifiers/bound_simplifier.h
+++ b/src/ast/simplifiers/bound_simplifier.h
@@ -40,6 +40,7 @@ class bound_simplifier : public dependent_expr_simplifier {
dep_intervals m_interval;
ptr_vector<expr> m_var2expr;
unsigned_vector m_expr2var;
+ expr_ref_vector m_trail;
mpq_buffer m_num_buffer;
var_buffer m_var_buffer;
unsigned m_num_reduced = 0;
@@ -71,6 +72,7 @@ class bound_simplifier : public dependent_expr_simplifier {
if (e != core_e)
m_expr2var.setx(core_e->get_id(), v, UINT_MAX);
m_var2expr.push_back(core_e);
+ m_trail.push_back(e);
}
return v;
}
@@ -100,6 +102,7 @@ public:
m_rewriter(m),
bp(nm, m_alloc, p),
m_interval(m.limit()),
+ m_trail(m),
m_num_buffer(nm) {
updt_params(p);
}