From 323e0e62705d31edc0ce06c6b4378c45c6b6184d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 1 May 2021 16:43:54 -0700
Subject: [PATCH] #5223

---
 src/ast/arith_decl_plugin.cpp | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index 68f37e3c5..a67464a92 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -898,7 +898,8 @@ bool arith_util::is_extended_numeral(expr* term, rational& r) const {
             continue;
         }
         if (is_mul(term)) {
-            rational r(mul), n(0);
+            r = mul;
+            rational n(0);
             for (expr* arg : *to_app(term)) {
                 if (!is_extended_numeral(arg, n))
                     return false;
@@ -907,7 +908,8 @@ bool arith_util::is_extended_numeral(expr* term, rational& r) const {
             return true;
         }
         if (is_add(term)) {
-            rational r(0), n(0);
+            rational n(0);
+            r = 0;
             for (expr* arg : *to_app(term)) {
                 if (!is_extended_numeral(arg, n))
                     return false;
@@ -921,8 +923,7 @@ bool arith_util::is_extended_numeral(expr* term, rational& r) const {
         if (is_sub(term, t1, t2) && 
             is_extended_numeral(t1, k1) &&
             is_extended_numeral(t2, k2)) {
-            r = k1 - k2;
-            r *= mul;
+            r = (k1 - k2) * mul;
             return true;
         }
         return false;