mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

#6971

Browse source 
clear m_a1, m_a2 before calls that may affect model.
This commit is contained in:
Nikolaj Bjorner 2023-11-01 03:35:54 -07:00
parent 3af2b36cd7
commit ea915e5b37
2 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/smt/arith_solver.cpp
View file

@ -1518,6 +1518,7 @@ namespace arith {
void solver::propagate_nla() {
if (m_nla) {
m_a1 = nullptr; m_a2 = nullptr;
m_nla->propagate();
add_lemmas();
lp().collect_more_rows_for_lp_propagation();

4
src/smt/theory_lra.cpp
View file

@ -2178,6 +2178,8 @@ public:
void propagate_nla() {
if (m_nla) {
m_a1 = nullptr;
m_a2 = nullptr;
m_nla->propagate();
add_lemmas();
lp().collect_more_rows_for_lp_propagation();
@ -3385,7 +3387,7 @@ public:
}
nlsat::anum const& nl_value(theory_var v, scoped_anum& r) const {
SASSERT(use_nra_model());
SASSERT(m_nla && m_nla->use_nra_model());
auto t = get_tv(v);
if (t.is_term()) {