From ca2ad66d03169b9cd1ad362d8e638dfa7b512844 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Nov 2019 10:49:35 -0800 Subject: [PATCH] treat division by 0 as non-linearity Signed-off-by: Nikolaj Bjorner --- src/ast/static_features.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index f216022f2..e5135347c 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -312,7 +312,7 @@ void static_features::update_core(expr * e) { case OP_IDIV: case OP_REM: case OP_MOD: - if (!is_numeral(to_app(e)->get_arg(1))) + if (!is_numeral(to_app(e)->get_arg(1), r) || r.is_zero()) m_num_non_linear++; break; }