From 47bd06338e6b614f022ea3d8e6351286de53e0d8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Mar 2020 11:54:24 -0700 Subject: [PATCH] fix #3283 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_nl.h | 4 ++-- src/smt/theory_utvpi_def.h | 5 ++++- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 025ec76d1..1e4bc1b96 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -934,8 +934,8 @@ bool theory_arith::propagate_linear_monomial(theory_var v) { new_lower = alloc(derived_bound, v, inf_numeral(k), B_LOWER); new_upper = alloc(derived_bound, v, inf_numeral(k), B_UPPER); } - SASSERT(new_lower != 0); - SASSERT(new_upper != 0); + SASSERT(new_lower); + SASSERT(new_upper); m_bounds_to_delete.push_back(new_lower); m_asserted_bounds.push_back(new_lower); m_bounds_to_delete.push_back(new_upper); diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index 48414e629..076fefda1 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -677,7 +677,10 @@ namespace smt { template bool theory_utvpi::enable_edge(edge_id id) { - return (id == null_edge_id) || (m_graph.enable_edge(id) && m_graph.enable_edge(id+1)); + return + (id == null_edge_id) || + (m_graph.enable_edge(id) && m_graph.enable_edge(id+1)) || + m_non_utvpi_exprs; } template