From 2af08a378d7759fc0a047125dadd80a295737c56 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 8 Jul 2017 18:21:47 -0700
Subject: [PATCH] avoid complaining about division by 0 as unhandled in
theory-lra
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/arith_decl_plugin.h | 2 ++
src/smt/theory_lra.cpp | 3 +++
2 files changed, 5 insertions(+)
diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index beb227c33..6d6da9ed5 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -275,7 +275,9 @@ public:
bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); }
bool is_mul(expr const * n) const { return is_app_of(n, m_afid, OP_MUL); }
bool is_div(expr const * n) const { return is_app_of(n, m_afid, OP_DIV); }
+ bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); }
bool is_idiv(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV); }
+ bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); }
bool is_mod(expr const * n) const { return is_app_of(n, m_afid, OP_MOD); }
bool is_rem(expr const * n) const { return is_app_of(n, m_afid, OP_REM); }
bool is_to_real(expr const * n) const { return is_app_of(n, m_afid, OP_TO_REAL); }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 2bd4844e8..9e4f544c1 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -292,6 +292,9 @@ namespace smt {
}
void found_not_handled(expr* n) {
+ if (a.is_div0(n)) {
+ return;
+ }
m_not_handled = n;
if (is_app(n) && is_underspecified(to_app(n))) {
m_underspecified.push_back(to_app(n));