From f9195c77a7ac88fea0bde163bf04256b969619f5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Jan 2019 09:46:04 -0800 Subject: [PATCH] remove not-handled clause from mod with non-numerals Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c9db3f6b0..01330269c 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -483,22 +483,6 @@ class theory_lra::imp { if (ctx().relevancy()) ctx().add_relevancy_dependency(n, mod); } else if (a.is_mod(n, n1, n2)) { - bool is_num = a.is_numeral(n2, r) && !r.is_zero(); - if (!is_num) { - found_not_handled(n); - } -#if 0 - else { - app_ref div(a.mk_idiv(n1, n2), m); - mk_enode(div); - theory_var w = mk_var(div); - theory_var u = mk_var(n1); - // add axioms: - // u = v + r*w - // abs(r) > v >= 0 - assert_idiv_mod_axioms(u, v, w, r); - } -#endif if (!ctx().relevancy()) mk_idiv_mod_axioms(n1, n2); } else if (a.is_rem(n, n1, n2)) {