From b75d81f3c2b878726982111dc48b9b4765ad7cca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 14 Apr 2023 16:38:33 -0700 Subject: [PATCH] fix #6690 --- src/sat/smt/arith_internalize.cpp | 6 ++++-- src/smt/theory_lra.cpp | 8 +++++--- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index d35f7995476..60ca9651a19 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -107,10 +107,12 @@ namespace arith { e = a.mk_idiv0(x, y); } else if (a.is_rem(n, x, y)) { - e = a.mk_rem0(x, y); + n = a.mk_rem(x, a.mk_int(0)); + e = a.mk_rem0(x, a.mk_int(0)); } else if (a.is_mod(n, x, y)) { - e = a.mk_mod0(x, y); + n = a.mk_mod(x, a.mk_int(0)); + e = a.mk_mod0(x, a.mk_int(0)); } else if (a.is_power(n, x, y)) { e = a.mk_power0(x, y); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 3b3e3dd79f4..657c48d389d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -315,11 +315,13 @@ class theory_lra::imp { else if (a.is_idiv(n, x, y)) { e = a.mk_idiv0(x, y); } - else if (a.is_rem(n, x, y)) { - e = a.mk_rem0(x, y); + else if (a.is_rem(n, x, y)) { + n = a.mk_rem(x, a.mk_int(0)); + e = a.mk_rem0(x, a.mk_int(0)); } else if (a.is_mod(n, x, y)) { - e = a.mk_mod0(x, y); + n = a.mk_mod(x, a.mk_int(0)); + e = a.mk_mod0(x, a.mk_int(0)); } else if (a.is_power(n, x, y)) { e = a.mk_power0(x, y);