From c431a100b76adda5e1f37dec7196c4f20d85c0b6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Apr 2020 21:31:01 -0700 Subject: [PATCH] fix #3707 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_dense_diff_logic_def.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 8793540bf..ae6288f69 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -146,7 +146,10 @@ namespace smt { SASSERT(m_autil.is_le(n) || m_autil.is_ge(n)); app * lhs = to_app(n->get_arg(0)); app * rhs = to_app(n->get_arg(1)); - SASSERT(m_autil.is_numeral(rhs)); + if (!m_autil.is_numeral(rhs)) { + found_non_diff_logic_expr(n); + return false; + } rational _k; m_autil.is_numeral(rhs, _k); numeral offset(_k);