fix Z3Prover#6326

NikolajBjorner · Sep 7, 2022 · 5322d4f · 5322d4f
1 parent adf6e98
commit 5322d4f
Show file tree

Hide file tree

Showing 2 changed files with 44 additions and 1 deletion.
diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c
@@ -2946,6 +2946,28 @@ void mk_model_example() {
     Z3_del_context(ctx);
 }
 
+void divides_example()
+{
+    Z3_context ctx;
+    Z3_solver s;
+    Z3_ast x, number;
+    Z3_ast c;
+
+    ctx    = mk_context();
+    s      = mk_solver(ctx);
+
+    x      = mk_int_var(ctx, "x");
+    number = mk_int(ctx, 2);
+
+    c      = Z3_mk_divides(ctx, number, x);
+    Z3_solver_assert(ctx, s, c);
+
+    check2(ctx, s, Z3_L_TRUE);
+
+    del_solver(ctx, s);
+    Z3_del_context(ctx);
+}
+
 /**@}*/
 /**@}*/
 
@@ -2955,6 +2977,7 @@ int main() {
 #ifdef LOG_Z3_CALLS
     Z3_open_log("z3.log");
 #endif
+    divides_example();
     display_version();
     simple_example();
     demorgan();

diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp
@@ -22,6 +22,8 @@ Revision History:
 #include "ast/arith_decl_plugin.h"
 #include "math/polynomial/algebraic_numbers.h"
 
+#include <iostream>
+
 #define MK_ARITH_OP(NAME, OP) MK_NARY(NAME, mk_c(c)->get_arith_fid(), OP, SKIP)
 #define MK_BINARY_ARITH_OP(NAME, OP) MK_BINARY(NAME, mk_c(c)->get_arith_fid(), OP, SKIP)
 #define MK_ARITH_PRED(NAME, OP) MK_BINARY(NAME, mk_c(c)->get_arith_fid(), OP, SKIP)
@@ -88,7 +90,25 @@ extern "C" {
     MK_ARITH_PRED(Z3_mk_gt,  OP_GT);
     MK_ARITH_PRED(Z3_mk_le,  OP_LE);
     MK_ARITH_PRED(Z3_mk_ge,  OP_GE);
-    MK_ARITH_PRED(Z3_mk_divides, OP_IDIVIDES);
+
+    Z3_ast Z3_API Z3_mk_divides(Z3_context c, Z3_ast n1, Z3_ast n2) {
+        Z3_TRY;
+        LOG_Z3_mk_divides(c, n1, n2);
+        RESET_ERROR_CODE();
+        rational val;
+        if (!is_expr(n1) || !mk_c(c)->autil().is_numeral(to_expr(n1), val) || !val.is_unsigned()) {
+            SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
+            RETURN_Z3(nullptr);
+        }
+        parameter p(val.get_unsigned());
+        expr* arg = to_expr(n2);
+        expr* a = mk_c(c)->m().mk_app(mk_c(c)->get_arith_fid(), OP_IDIVIDES, 1, &p, 1, &arg);
+        mk_c(c)->save_ast_trail(a);
+        check_sorts(c, a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
     MK_UNARY(Z3_mk_int2real, mk_c(c)->get_arith_fid(), OP_TO_REAL, SKIP);
     MK_UNARY(Z3_mk_real2int, mk_c(c)->get_arith_fid(), OP_TO_INT, SKIP);
     MK_UNARY(Z3_mk_is_int,   mk_c(c)->get_arith_fid(), OP_IS_INT, SKIP);