From ab43d2dcf1d460f58996e24c6d1f09c1387c9331 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 29 Jan 2025 04:29:38 -0800
Subject: [PATCH] fix semantics of check-int64 div operation to align with
 smtlib semantics

---
 src/ast/sls/sls_context.cpp |  5 +++++
 src/util/checked_int64.h    | 10 ++++++++++
 2 files changed, 15 insertions(+)

diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp
index 0ef4d8a04..c58be15d1 100644
--- a/src/ast/sls/sls_context.cpp
+++ b/src/ast/sls/sls_context.cpp
@@ -25,6 +25,7 @@ Author:
 #include "ast/sls/sls_seq_plugin.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_pp.h"
+#include "ast/for_each_expr.h"
 #include "smt/params/smt_params_helper.hpp"
 
 namespace sls {
@@ -208,6 +209,10 @@ namespace sls {
 
             if (bad_model) {             
                 IF_VERBOSE(0, verbose_stream() << lit << " " << a->get_id() << " " << mk_bounded_pp(a, m) << " " << eval_a << "\n");
+                TRACE("sls", s.display(tout << lit << " " << a->get_id() << " " << mk_bounded_pp(a, m) << " " << eval_a << "\n");
+                for (expr* t : subterms::all(expr_ref(a, m))) 
+                    tout << "#" << t->get_id() << ": " << mk_bounded_pp(t, m) << " := " << ev(t) << "\n";
+                );
                 throw default_exception("failed to create a well-formed model");
             }
         }
diff --git a/src/util/checked_int64.h b/src/util/checked_int64.h
index ec71bef13..aab741682 100644
--- a/src/util/checked_int64.h
+++ b/src/util/checked_int64.h
@@ -300,6 +300,16 @@ template<bool CHECK>
 inline checked_int64<CHECK> div(checked_int64<CHECK> const& a, checked_int64<CHECK> const& b) {
     checked_int64<CHECK> result(a);
     result /= b;
+    if (a < 0) {
+        checked_int64<CHECK> r(a);
+        r %= b;
+        if (r != 0) {
+            if (b < 0)
+                result += 1;
+            else
+                result -= 1;
+        }
+    }
     return result;
 }