From 988a46dbc434c14aa093cc71bcf30a420e2eb9b5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Aug 2024 17:32:58 -0700 Subject: [PATCH] fix division by 0 Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_arith_base.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index 8ce608624..84fd8fc9b 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -1826,6 +1826,9 @@ namespace sls { auto x0 = div(a, num_t(k)); + if (x0 == 0) + return x0; + auto x1 = div((x0 * num_t(k - 1)) + div(a, power_of(x0, k - 1)), num_t(k)); while (x1 < x0) {