Active questions tagged z3 - Stack Overflow

Set membership relation in z3

2013-04-21T22:44:54Z

I wanted to define a membership relation in Z3 with C++ APIs. I thought of doing it in the following way:

z3::context C;
z3::sort I = C.int_sort();
z3::sort B = C.bool_sort();
z3::func_decl InSet = C.function("f", I, B);

z3::expr e1 = InSet(C.int_val(2)) == C.bool_val(true);
z3::expr e2 = InSet(C.int_val(3)) == C.bool_val(true);
z3::expr ite  = to_expr(C, Z3_mk_ite(C, e1, C.bool_val(true),
    Z3_mk_ite(C,e2,C.bool_val(true),C.bool_val(false))));
errs() << Z3_ast_to_string(C,ite);

In this example the set is composed by the integer 2 and 3. I am sure there is a better way to define a relation, in particular a set membership relation, but I am really a Z3 rookie. Does anyone know the best one?

How to use tuples in SMT-lib?

2021-05-21T07:53:12Z

I am quite sure that it should be possible to describe tuples using SMT-lib syntax, especially for the Z3 solver. However, I can't really find a way of doing so. The only thing I found is this documentation page, but I don't get how to use it in z3 -in.

My struggles so far:

(declare-const t (Prod Int Bool))
(error "line 1 column 19: unknown sort 'Prod'")
(declare-const t (Tuple Int Bool))
(error "line 2 column 18: unknown sort 'Tuple'")
(declare-const t (Pair Int Bool))
(error "line 3 column 18: unknown sort 'Pair'")

What tactics/strategies to use for mixed complementarity problems?

2026-04-20T12:18:37Z

I would appreciate your input on a hypothesis I am currently working on: Exploiting the logical condition of mixed complementarity problems (MCP) by using (constraint) propagation techniques. I would like to solve the MCP as a system of equations which includes the complementarity condition as a propositional formula for which I am using Z3. How can I influence and direct the search for a feasible solution?

Setting

My test bed is a bimatrix game, which is a simultaneous game for two players in which each player has a finite number of possible actions. The payoffs resulting from actions are described by two matrices. The payoffs of player 1 are given by

A = \begin{bmatrix} 3 & 3 \\ 2 & 5 \\ 0 & 6 \end{bmatrix}

with strategies M = \set{1, 2, 3} (which are the rows of A). The payoffs of player 2 are given by

B = \begin{bmatrix} 3 & 2 \\ 2 & 6 \\ 3 & 1 \end{bmatrix}

with strategies N = \set{4, 5} (which are the columns of B).

My chosen approach is to frame the bimatrix game as a feasibility problem, to find a solution in the form of a Nash equilibrium (that is, each player's chosen action is the payoff maximising action given the other player's chosen action). For the feasibility problem, I am using a set of variables for mixed strategies x_{1}, x_{2}, x_{3} \in \mathbb{R}_{+} for player 1 and y_{4}, y_{5} \in \mathbb{R}_{+} for player 2. Additionally, there are variables for the players' expected payoffs u \in [0, \max(A)] for player 1 and v \in [0, \max(B)] for player 2.

Problem

The payoff inequalities are given by

\begin{align*}
(Ay)_{i} \leq u \forall i \in M (1),\\
(B^{\top}x)_{j} \leq v \forall j \in N (2).
\end{align*}

Since the mixed strategies represent a probability distribution, we also have

\begin{align*}
\sum_{i \in M} x_{i} = 1 (3),\\
\sum_{j \in N} y_{j} = 1 (4).
\end{align*}

Lastly, the complementarity conditions which are the following bilinear terms:

x_{i} (u - (Ay)\_{i}) = 0 \forall i \in M (5)

for player 1. Similarly for player 2, we have

y_{j} (v - (B^{\top} x)_{j}) = 0 \forall j \in N (6).

These bilinear terms express that the player's mixed strategy vector is orthogonal to their expected payoff vector. In other words, a player plays an action with positive probability, or the respective expected payoff equals the expected payoff by playing this strategy.

Hypothesis

I express the complementarity conditions (5) and (6) as logical disjunctions:

(x\_{i} = 0) \lor (u - (Ay)_{i} = 0) \forall i \in M (7)

for player 1 and

(y_{j} = 0) \lor (v - (B^{\top} x)_{j} = 0) \forall j \in N (8)

for player 2. Then I rewrite disjunctions (7) and (8) as implications

\begin{align*}
(x_{i} > 0) \Rightarrow (u - (Ay)_{i} = 0) \forall i \in M (9),\\
(y_{j} > 0) \Rightarrow (v - (B^{\top}x)_{j} = 0) \forall j \in N (10),
\end{align*}

respectively. Alternatively, implications (9) and (10) can be written with a double negation in the antecedence:

\begin{align*}
(x_{i} != 0) \Rightarrow (u - (Ay)_{i} = 0) \forall i \in M (11),\\
(y_{j} != 0) \Rightarrow (v - (B^{\top}x)_{j} = 0) \forall j \in N (12),
\end{align*}

My idea behind it is that the complementarity problem can be solved by backtracking on binary cases of the mixed strategy variables: An action is played with either zero probability or positive probability. If it is played with positive probability, then the expected payoff of the associated action must equal the total expected payoff.
In other words, I want to avoid a search in the continuous space of mixed strategies to find a point where all equations (1)–(6) (partly nonlinear) hold.

Solution Approach

It is worth noting that every bimatrix game has a Nash equilibrium in mixed strategies. This can be done by applying the Lemke-Howson algorithm, which is a pivoting technique on the Best Response polytopes of A and B.
Yet, I have chosen a SAT/CSP/SMT approach because I expect it to be a more flexible modelling framework to allow for additional side-constraints or optimising the mixed strategy vectors with respect to some objective.

I ended up with using Z3 and Choco+IBEX, since most other CSP solvers focus primarily on discrete domains (while I need continuous domains for x and y). However, I dropped Choco+IBEX, as it does not scale as well as Z3 does for problems with matrices of size up to 150-by-150. This is probably because Choco+IBEX finds sets of intervals whereas Z3 focuses on sets of points.

Experience

Z3, on default settings, allows me to solve the system of equations (1)–(4) plus the complementarity conditions as random problems of size up to 150-by-150 matrices with integer payoffs [0,10]. Quick (naive) experiments (with different seeds) showed that it might matter for Z3 how the complementarity constraints are implemented using

disjunctions (7) and (8), Z3 terminated after between 0.66 and 10 seconds,
implications (9) and (10), Z3 terminated after between 1.2 and 15 seconds, and
implications (11) and (12), Z3 terminated after between 1.2 and 8 seconds.

From MIP solvers, I also know that they can be tuned to decrease the computation time of some problems, like branching strategies, variable selection, add callbacks, etc. Is it possible to do similarly with Z3?
In particular, there is the Porter, Nudelman & Shoham (2006) article to solve n-player bimatrix games by searching the combinatorial space of actions. It does so by manually implementing a backtracking with arc-consistency-based pruning algorithm which wraps around a feasibility problem containing equations (1)–(4). Using this constraint propagation technique enhances the computation time significantly compared to the Lemke-Howson algorithm.

Questions

I would like to know if it is possible to 'internalise' what Porter, Nudelman & Shoham does into a configuration of Z3. Namely:

Can I instruct Z3 to prioritise small true assignments (i.e., \min |\{ x_{i} : x_{i} > 0, \forall i \in M \cup N \}|)?
Can I instruct Z3 to prioritise balanced true assignments (i.e., \min (|\{ x_{i} : x_{i} > 0, \forall i \in M \}| - |\{ y_{i} : y_{j} > 0 \forall j \in N \}|))?
Does it make sense to adjust the arbitrary precision by, say, set_option(precision=16) (Python API)?
Does it make sense to specify an engine by including SolveFor('QF_LRA') (Python API)?
Should I choose a different SMT solver, such as cvc5 or MathSAT5?

References

I have read through:

https://z3prover.github.io/papers/programmingz3.html
Scalability of z3
Have Z3 prioritize certain Boolean variables when branching/searching for a model
and tried to find answers to questions relating to performance, tuning, etc. under the z3 tag.
Porter, Nudelman, Shoham (2006): https://doi.org/10.1016/j.geb.2006.03.015

How to determine symbolic relationship between different variables (rather than concrete values)

2026-04-17T22:24:01Z

I need a way to determine programmatically the symbolic relationship between variables in an equation

For example, forall x, given 3ax - bx = 0, I want to determine that b must be equal to 3a. When I attempt to synthesize these values using something like Z3 I get concrete values rather than symbolic expressions, and the closest thing I've found thus far is Z3's get_implied_equalities. But that appears to require already knowing what the expected equality is, which I would not.

I know this wasn't possible in the past using Z3 (See: Symbolic variables in z3), but I don't know if that limitation is Z3 specific or a technical challenge across the board. I'm open to using any tool (although one with a C interface I could ffi to would be ideal)

Checking if a graph is connected with Z3

2026-02-16T17:15:51Z

I'm trying to code a solver for the chinese postman problem using z3. I have to check two things to see if there is already a solution available:

if every node has even degree
if the graph is connected

The first is easy, but I don't know how to check the second. I feel like I should use the Transitive closure but I don't know how to implement the function in the code. I'm assuming that every edge is undirected.

from z3 import *

solver = Solver()

nodes = ["A", "B", "C", "D", "E", "F", "G"]
numnodes = 7

edges = [ ["A", "B", 5], ["B", "C", 1], ["C", "D", 7], ["D", "A", 9], ["E", "F", 3], ["F", "G", 2], ["G", "E", 3]]

degree = [0] * numnodes

for x, y, z in edges:
    degree[nodes.index(x)] +=1
    degree[nodes.index(y)] +=1


for i in range(numnodes):
    solver.add(degree[i] % 2 == 0)

if solver.check() == sat:
    print("Eulerian circuit exists")
else:
    print("No Eulerian circuit exists")

This is what I'v written so far. Edges are defined as [start node, end node, cost] .

What's the meaning of uninterpreted sorts with non-zero arity and how do I get them in the Z3 C API?

2025-12-08T14:14:49Z

SMT-LIB supports declaring uninterpreted sorts with an "arity" argument such as:

(declare-sort MySort 2)

Then one can declare functions and constants using that sort, which must be given some sort arguments.

(declare-const x (MySort Int Real))

I'm not really sure how I should use this feature. Is any instantiation of (MySort X Y) a different uninterpreted sort altogether? Given that I cannot declare type-parametric functions, what's the intended usage of this feature?

Also, while Z3 supports it when parsing SMT-LIB files, it seems I cannot find the corresponding feature in the C API. The Z3_mk_uninterpreted_sort() function does not take an arity parameter and I cannot find other functions with this purpose.

So how do I use parametric uninterpreted sorts in SMT-LIB and how do I get them from the Z3 C API?

Looking for practical examples of SMT Z3 usecases (like DbC) and open source alternative to Z3? [closed]

2011-01-06T13:52:34Z

I have got interested in and looking for practical examples of SMT Z3 usage (like DbC) with code and open source alternatives to this tool. So, in fact, I am interested in similar Z3 formal solving tools, but:

it must be open source
provide both low-level (API) and high-level (Text scripting) interaction
support SMT-LIB
suitable(usable) in tools/written in/for languages as Java, python, ruby, Vala, and not Haskell
has stable (usable in practice) tools based on it, like design by contract (DbC), static type verification, etc.

According to SMT-LIB homepage (see bit.ly bundle for details) the list of 2010 SMT solvers is: "Alt-Ergo, Barcelogic, Beaver, Boolector , CVC3, DPT, MathSAT, OpenSMT, SatEEn, Spear, STP, SWORD, UCLID, veriT, Yices, Z3."

Please give any feedback on using any of them in practice (code examples are the best)?

Finally, any information on comparison of it with GHC possibilities would be useful, but only in case there is an implementation example (not a language "feature").

Solving "The Hardest Logic Puzzle Ever" via z3

2025-06-27T11:10:51Z

I am trying to solve The Hardest Logic Puzzle Ever, about 3 gods. So far, I have written the following code, but it returns unsat. I am expressing questions as functions and trying to use z3 to find functions that satisfy the conditions of the problem. Answers from a random god are random, and I used an uninterpreted variable to formalize that behavior. Can someone help find the issue in my code or provide z3 based solution that returns the correct answer to the problem?

from z3 import *

Tr=0
Fa=1
Ra=2

def GetArrayElement(arr,index):
    current_else = arr[0]
    for i in range(1,len(arr)):
        current_else = If(index==i,arr[i],current_else)      
    return current_else

def PrintFunc(m,func,args,current_val=[]):
    if len(args)==0:
        print(current_val,m.eval(func(*current_val)))
        return
    for value in args[0]:
        PrintFunc(m,func,args[1:],current_val+[value])

s=Solver()

gods = [ Int("god_%s" % (j+1)) for j in range(3)  ]


yes_answer=Bool("yes")
no_answer=Bool("no")


question1 = Function("question_1", IntSort(),IntSort(),IntSort(),BoolSort(),BoolSort(),                         BoolSort()) 
question2 = Function("question_2", IntSort(),IntSort(),IntSort(),BoolSort(),BoolSort(),BoolSort(),              BoolSort()) 
question3 = Function("question_3", IntSort(),IntSort(),IntSort(),BoolSort(),BoolSort(),BoolSort(),BoolSort(),   BoolSort()) 
determine_god = Function("determine_god", BoolSort(),BoolSort(),IntSort(),                                      IntSort()) 

who_to_ask1 = Function("who_to_ask1",               IntSort()) 
who_to_ask2 = Function("who_to_ask2",               IntSort()) 
who_to_ask3 = Function("who_to_ask3", BoolSort(),   IntSort()) 

x=Bool("x")
s.add(0<=who_to_ask1(),who_to_ask1()<3)
s.add(0<=who_to_ask2(),who_to_ask2()<3)
s.add(ForAll([x],And(0<=who_to_ask3(x),who_to_ask3(x)<3)))

answers_of_random_god = Bools("unkn1 unkn2 unkn3")

def GetAnswer(question,question_id,god):
    return  If(god==Tr,
               If(question,yes_answer,no_answer),
            If(god==Fa,
               If(question,no_answer,yes_answer),
            answers_of_random_god[question_id]))
# def GetAnswer(question,question_id,god):
#     return  If(question,yes_answer,no_answer)

answer1=GetAnswer(question1(gods[0],gods[1],gods[2],yes_answer,no_answer),0,GetArrayElement(gods,who_to_ask1()))
answer2=GetAnswer(question2(gods[0],gods[1],gods[2],yes_answer,no_answer,answer1),1,GetArrayElement(gods,who_to_ask2()))
answer3=GetAnswer(question3(gods[0],gods[1],gods[2],yes_answer,no_answer,answer1,answer2),2,GetArrayElement(gods,who_to_ask3(answer1==answer2)))



z=Int("z")
s.add(ForAll(gods+[no_answer,yes_answer,z]+answers_of_random_god,Implies(And(And([And(0<=god,god<3) for god in gods]),Distinct(gods),Distinct(yes_answer,no_answer),0<=z,z<3), 
                                                   
                                                   And(GetArrayElement(gods,z)==determine_god(answer1==answer2,answer1==answer3,z)))
))
#print(s)
if s.check() == sat:
    m = s.model()
    print(m)

print(s.check())

Z3: unclear model

2025-09-29T08:19:30Z

When I send Z3 the trivial:

(declare-fun M (Int) Int)
(check-sat)
(get-value (M))

Z3 answers:

((M (_ as-array M)))

How shall I interpret this answer?

Encoding of first order differential equation as First order formula

2012-08-13T01:00:11Z

Can somebody help me in pointing out what will be the best encoding of following equation using first order formula so as to give it as input to the SMT solver??

x`=Ax+b

Problems proving trivial things involving shift operators using Frama-C WP

2025-08-31T16:22:21Z

I have this very simple example.

/*@
  requires a >= 0 && a <= 2;
  assigns \nothing;
  ensures \result < 10;
*/
int bob(int a) {
  return 1 << a;
}

When I try to prove this with both Alt-Ergo and z3 it times out

$ frama-c test.c -wp -wp-prover="Alt-Ergo,z3" -wp-status
[kernel] Parsing test.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Timeout] typed_bob_ensures (Qed 1ms) (Alt-Ergo) (Cached)
[wp] [Cache] found:2
[wp] Proved goals:    3 / 4
  Terminating:     1
  Unreachable:     1
  Qed:             1 (0.72ms)
  Timeout:         1
------------------------------------------------------------
  Function bob
------------------------------------------------------------

Goal Post-condition (file test.c, line 110) in 'bob':
Let x = lsl(1, a).
Assume {
  Type: is_sint32(a) /\ is_sint32(x).
  (* Pre-condition *)
  Have: (0 <= a) /\ (a <= 2).
}
Prove: x <= 9.
Prover Alt-Ergo 2.6.2 returns Timeout (Qed:1ms) (2s) (cached)
Prover Z3 4.8.12 returns Timeout (Qed:1ms) (2s) (cached)

------------------------------------------------------------

According to the WP manual there is a shift strategy that should be able to transform lsl(a,k) to a*2^k and with that transformation it feels like this should be automatically provable (Right??)

I have tried defining a strategy with:

/*@
@strategy shift:
  \tactic("Wp.shift");
*/

/*@
  requires a >= 0 && a <= 2;
  assigns \nothing;
  ensures \result < 10;
*/
int bob(int a) {
  return 1 << a;
}


//@proof shift : bob;

And I have tried applying the strategy with the -wp-strategy="shift" flag as well but i has had no effect.

Is there any other explicit thing that I have to do in order to get any of the provers to handle the << operator?

If clause in Z3py without the else

2022-04-02T14:04:07Z

How do we write an If('condition', x, y) clause in Z3py if we don't have the 'else' part ?

Z3 python simplify without monomials on bitvectors

2025-07-25T22:35:40Z

I have the following expression:

a = z3.BitVec('a', 32)
b = z3.BitVec('b', 32)

e = a - b < z3.BitVecVal(0, 32)

z3.simplify returns:

Not(0 <= a + 4294967295*b)

I even tried with options such as som=False but to no avail, what can I do to prevent this rewrite with monomials?

z3 sort mismatch for different bytes of the same variable [closed]

2021-12-06T18:20:47Z

I'm simulating the behaviour of an algorithm using z3 python package, however I'm encountering problems using a bitwise XOR.

At first I define

    class State:
        def __init__(self):
            self.state = [0] * 0x270
            self.index = 0

    def mag(i):
        return z3.If(i == 0, 0x0, 0x9908b0df)

seed = z3.BitVec('seed', 32)
s= State()

And the script goes on, however when I run the Solver I get a z3.z3types.Z3Exception: sort mismatch caused by trying to execute the __xor__ in the line

s.state[i] = s.state[i + 0x18d] ^ ((s.state[i + 1] & 0x7fffffff | s.state[i] & 0x80000000) >> 1) ^ mag((s.state[1] & 1) *8)

Here every entry in s.state depends on the symbolic value of the seed.

Indexing array by bv32 in Dafny causes timeout

2025-07-07T03:24:26Z

ghost predicate AllZero(a: array<int>, n: bv32)
    reads a {
    a.Length == (n as int) &&
    (forall i :: 0 <= i < n ==> a[i] == 0)
}

I need to use the result of binary arithmetic to index an array. However, I found that even trivial array indexing expressions take forever to verify. Changing the type of n to int makes the code verify instantly.

What auxiliary lemma should I add to make it work?

Control recursive function evaluation depth in eval

2025-07-04T19:24:51Z

As an exercise, to get a good idea of what Z3 can and can't do, I was trying to solve a "coraline" puzzle. This is a rectangular grid, where each square is a graph node of degree two: each edge is to an adjacent node. So a square could be top-left, top-right, bottom-left, bottom-right, right-left, or top-bottom. A coraline problem specifies the grid size, and these values for some subset of the squares. The solution must be a path through all the squares -- a Hamiltonion path in the graph view.

My thought was to encode the connectivity constraints, and then encode the "single path" idea by defining an order on coordinates, and defining a recursive function that find the minimum coordinate reachable from a given coordinate. The single-path constraint would then be that this function yields (0, 0) for all squares.

Well, that doesn't work (at least not yet). But I have some simpler questions before I ask why.

For a 4x2 grid, with no initial conditions, if I comment out the single-path constraint, it finds a satisfying solution. The one it finds happens to satisfy the single-path constraint. The code is:

(declare-datatypes () ((SquareType TL TR BL BR TB RL)))
(define-fun square-to-string ((st SquareType)) String
        (ite (= st TL) "TL"
         (ite (= st TR) "TR"
              (ite (= st BL) "BL"
               (ite (= st BR) "BR"
                (ite (= st RL) "RL"
                     (ite (= st TB) "TB"
                      "unknown")))))))

(define-sort AISQ () (Array Int SquareType))
(define-sort Board () (Array Int AISQ))

(declare-const Width Int)
(declare-const Height Int)

(define-fun is-x-index ((x Int)) Bool (and (>= x 0) (< x Width)))
(define-fun is-y-index ((y Int)) Bool (and (>= y 0) (< y Height)))

(define-fun get-square ((b Board) (x Int) (y Int)) SquareType
        (select (select b x) y))

(define-fun square-constraint ((b Board) (x Int) (y Int)) Bool
        (and
         (implies (and (> x 0) (or (= (get-square b x y) TL)
                       (= (get-square b x y) BL)
                       (= (get-square b x y) RL)))
              (or (= (get-square b (- x 1) y) TR)
              (= (get-square b (- x 1) y) BR)
              (= (get-square b (- x 1) y) RL)))
         (implies (= x 0)
              (or (= (get-square b x y) TR)
              (= (get-square b x y) BR)
              (= (get-square b x y) TB)
              ))

         (implies (and (< x (- Width 1)) (or (= (get-square b x y) TR)
                         (= (get-square b x y) BR)
                         (= (get-square b x y) RL)))
              (or (= (get-square b (+ x 1) y) TL)
              (= (get-square b (+ x 1) y) BL)
              (= (get-square b (+ x 1) y) RL)))
         (implies (= x (- Width 1))
              (or (= (get-square b x y) TL)
              (= (get-square b x y) BL)
              (= (get-square b x y) TB)
              ))
         
         (implies (and (> y 0) (or (= (get-square b x y) TR)
                       (= (get-square b x y) TL)
                       (= (get-square b x y) TB)))
              (or (= (get-square b x (- y 1)) BL)
              (= (get-square b x (- y 1)) BR)
              (= (get-square b x (- y 1)) TB)))
         (implies (= y 0)
              (or (= (get-square b x y) BR)
              (= (get-square b x y) BL)
              (= (get-square b x y) RL)))

         (implies (and (< y (- Height 1)) (or (= (get-square b x y) BR)
                          (= (get-square b x y) BL)
                          (= (get-square b x y) TB)))
              (or (= (get-square b x (+ y 1)) TL)
              (= (get-square b x (+ y 1)) TR)
              (= (get-square b x (+ y 1)) TB)))
         (implies (= y (- Height 1))
              (or (= (get-square b x y) TR)
              (= (get-square b x y) TL)
              (= (get-square b x y) RL)
              ))
         ))

;;; LeftTopMin
(declare-datatypes () ((Coord (mk-coord (getx Int) (gety Int)))))

(declare-datatypes () ((Dir TDir BDir RDir LDir)))

(define-fun dir-2-str ((dir Dir)) String
        (ite (= dir TDir) "T"
         (ite (= dir BDir) "B"
              (ite (= dir RDir) "R" "L"))))

(define-fun coord-lt ((c0 Coord) (c1 Coord)) Bool
        (or (< (getx c0) (getx c1))
        (and (= (getx c0) (getx c1))
             (< (gety c0) (gety c1)))))

(define-fun min-coord ((c0 Coord) (c1 Coord)) Coord
        (ite (coord-lt c0 c1) c0 c1))

(define-fun out-dir ((st SquareType) (inDir Dir)) Dir
        (ite (= st TL)
         (ite (= inDir TDir) LDir TDir)
         (ite (= st TR)
              (ite (= inDir TDir) RDir TDir)
              (ite (= st BL)
               (ite (= inDir BDir) LDir BDir)
               (ite (= st BR)
                (ite (= inDir BDir) RDir BDir)
                (ite (= st RL)
                     (ite (= inDir RDir) LDir RDir)
                     (ite (= inDir TDir) BDir TDir)))))))

;; Pick a direction that is one of the dirs of the SqureType
(define-fun pick-dir ((st SquareType)) Dir
        (ite (or (= st TL) (= st TR) (= st TB)) TDir
         (ite (or (= st BL) (= st BR)) BDir
              RDir)))

;; The reverse of the dir.
(define-fun reverse-dir ((dir Dir)) Dir
  (ite (= dir TDir) BDir
       (ite (= dir BDir) TDir
        (ite (= dir RDir) LDir RDir))))

;; The x value of the next square to consider (given x and, nextDir,
;; the direction in which to leave the current square).
(define-fun next-x ((x Int) (nextDir Dir)) Int
        (ite (= nextDir RDir)
         (+ x 1)
         (ite (= nextDir LDir)
              (- x 1)
              x)))
;; The y value of the next square to consider (given y and, nextDir,
;; the direction in which to leave the current square).
(define-fun next-y ((y Int) (nextDir Dir)) Int
        (ite (= nextDir TDir)
         (- y 1)
         (ite (= nextDir BDir)
              (+ y 1)
              y)))

(define-fun-rec min-coord-in-cc-work
    ((b Board)
     (cur Coord) ;; The coordinate of the current square to consider.
     (in Dir)  ;; The direction -- on of the two dirs of the square's value --
     ;; at which the path reaches the square.
     (start Coord) ;; The start of the path
     (min Coord)) ;; The min coord observed on the path so far.
  Coord
  (let ((x (getx cur)) (y (gety cur)))
    (let ((st (get-square b x y)))
      (let ((nextDir (out-dir st in)))
    (let ((nextX (next-x x nextDir))
          (nextY (next-y y nextDir)))
      (ite (= cur start)
           min
           (min-coord-in-cc-work b (mk-coord nextX nextY)
                     (reverse-dir nextDir)
                     start (min-coord min cur))))))))

;; Do we reach all the coords?
(declare-datatypes ()
           ((NextInputs (mk-inputs (getCoord Coord) (getDir Dir)))))



(define-fun min-coord-in-cc ((b Board) (c Coord))
  Coord
  (let ((x (getx c)) (y (gety c)))
    (let ((st (get-square b x y)))
      (let ((nextDir (out-dir st (pick-dir (get-square b (getx c) (gety c))))))
    (min-coord-in-cc-work
     b
     (mk-coord (next-x (getx c) nextDir)
           (next-y (gety c) nextDir))
     (reverse-dir nextDir)
     c c)))))

(define-fun is-solution ((b Board))
  Bool
  (forall ((x Int) (y Int))
      (implies (and (is-x-index x)
            (is-y-index y))
           (and
            (square-constraint b x y)
            ; (= (min-coord-in-cc b (mk-coord x y)) (mk-coord 0 0))
            ))))


(declare-const b0 Board)

(assert (= Width 4))
(assert (= Height 2))
(assert (is-solution b0))
(check-sat)

(echo "row 0")
(eval (square-to-string (get-square b0 0 0)))
(eval (square-to-string (get-square b0 1 0)))
(eval (square-to-string (get-square b0 2 0)))
(eval (square-to-string (get-square b0 3 0)))

(echo "row 1")
(eval (square-to-string (get-square b0 0 1)))
(eval (square-to-string (get-square b0 1 1)))
(eval (square-to-string (get-square b0 2 1)))
(eval (square-to-string (get-square b0 3 1)))

(This code makes the perhaps-unfortunate choice that the y coordinates grow "downwards" (wrt the Top/Bottom convention) -- apologies.) When I run this I get:

sat
row 0
"BR"
"RL"
"RL"
"BL"
row 1
"TR"
"RL"
"RL"
"TL"

If I comment out the

(assert (is-solution b0))

constraint, and instead assume the solution found:

(assert (= (select (select b0 0) 0) BR))
(assert (= (select (select b0 1) 0) RL))
(assert (= (select (select b0 2) 0) RL))
(assert (= (select (select b0 3) 0) BL))
(assert (= (select (select b0 0) 1) TR))
(assert (= (select (select b0 1) 1) RL))
(assert (= (select (select b0 2) 1) RL))
(assert (= (select (select b0 3) 1) TL))

then I can verify that my min-coord-in-cc function is working properly:

(eval (min-coord-in-cc b0 (mk-coord 0 0)))
(eval (min-coord-in-cc b0 (mk-coord 1 0)))
(eval (min-coord-in-cc b0 (mk-coord 2 0)))
(eval (min-coord-in-cc b0 (mk-coord 3 0)))
(eval (min-coord-in-cc b0 (mk-coord 0 1)))
(eval (min-coord-in-cc b0 (mk-coord 1 1)))
(eval (min-coord-in-cc b0 (mk-coord 2 1)))
(eval (min-coord-in-cc b0 (mk-coord 3 1)))

yields what I expect:

(mk-coord 0 0)
(mk-coord 0 0)
(mk-coord 0 0)
(mk-coord 0 0)
(mk-coord 0 0)
(mk-coord 0 0)
(mk-coord 0 0)
(mk-coord 0 0)

However, if do this printing of min-coord-in-cc values using the (same!) solution found via the is-solution constraint, the expression returned is much more complicated. Here is the first one:

(let ((a!1 (lambda ((x!1 Int))
             (let ((a!1 (ite (and (<= 1 x!1) (not (<= 2 x!1)))
                             ((as const (Array Int SquareType)) RL)
                             (store ((as const (Array Int SquareType)) RL) 5 TL))))
             (let ((a!2 (ite (<= 1 x!1)
                             (ite (<= 3 x!1)
                                  (store ((as const (Array Int SquareType)) TL)
                                         0
                                         BL)
                                  a!1)
                             (store ((as const (Array Int SquareType)) TR) 0 BR))))
               (ite (and (not (<= 3 x!1)) (<= 2 x!1))
                    ((as const (Array Int SquareType)) RL)
                    a!2)))))
      (a!11 (and (= (getx (mk-coord 0 0)) (getx (mk-coord 1 0)))
                 (< (gety (mk-coord 0 0)) (gety (mk-coord 1 0))))))
(let ((a!2 (select (select a!1 (getx (mk-coord 1 0))) (gety (mk-coord 1 0))))
      (a!12 (or (< (getx (mk-coord 0 0)) (getx (mk-coord 1 0))) a!11)))
(let ((a!3 (ite (= a!2 BR)
                (ite (= LDir BDir) RDir BDir)
                (ite (= a!2 RL)
                     (ite (= LDir RDir) LDir RDir)
                     (ite (= LDir TDir) BDir TDir)))))
(let ((a!4 (ite (= a!2 TR)
                (ite (= LDir TDir) RDir TDir)
                (ite (= a!2 BL) (ite (= LDir BDir) LDir BDir) a!3))))
(let ((a!5 (ite (= a!2 TL) (ite (= LDir TDir) LDir TDir) a!4)))
(let ((a!6 (ite (= a!5 LDir) (- (getx (mk-coord 1 0)) 1) (getx (mk-coord 1 0))))
      (a!8 (ite (= a!5 BDir) (+ (gety (mk-coord 1 0)) 1) (gety (mk-coord 1 0))))
      (a!10 (ite (= a!5 TDir)
                 BDir
                 (ite (= a!5 BDir) TDir (ite (= a!5 RDir) LDir RDir)))))
(let ((a!7 (ite (= a!5 RDir) (+ (getx (mk-coord 1 0)) 1) a!6))
      (a!9 (ite (= a!5 TDir) (- (gety (mk-coord 1 0)) 1) a!8)))
  (ite (= (mk-coord 1 0) (mk-coord 0 0))
       (mk-coord 0 0)
       (min-coord-in-cc-work
         a!1
         (mk-coord a!7 a!9)
         a!10
         (mk-coord 0 0)
         (ite a!12 (mk-coord 0 0) (mk-coord 1 0)))))))))))

Given the fact that it found the right solution, it seems like it ought to be able to evalutate this. Looking just at the end of the expression, shouldn't it (for example) be able to decide the

  (ite (= (mk-coord 1 0) (mk-coord 0 0))

It seems like deciding that would make this expression tail-recursive. Am I hitting some sort of limit on recursion depth here? Is there some way to control that?

How to use SMT tools to prove a simple theorem involving modulo [closed]

2025-06-24T15:03:05Z

I am trying to prove or refute the following:

   ((pid+1)%NP + i)%NP = (pid + i + 1)%NP

assuming pid, i, and NP are integers, 0≤pid<NP, and 0≤i. I think it's true, but in any case, I cannot get any SMT tool to prove or refute it.

Here is how I expressed the problem in SMT2:

(declare-const i Int)
(declare-const pid Int)
(declare-const NP Int)
(assert (<= 0 pid))
(assert (< pid NP))
(assert (<= 0 i))
(assert (not
  (= (mod (+ (mod (+ pid 1) NP) i) NP)
     (mod (+ pid i 1) NP))))
(check-sat)

I think it should return nsat, but neither CVC5 nor Z3 ever returns on this input. Any hints?

Z3 Lookup sorts with Cpp API without Constructors Definitions

2025-06-17T00:26:47Z

I'm currently trying to get information in some way of all the sorts present in an smt2 file, via the Cpp API. As I want to retrieve the values that are assigned to the sorts in the formula and assuming that there are no constructors for them defined. While I was following this logic I found the m.get_func_decl(). Which made it possible to retrieve the sorts of the argument functions. With no constructors which is what I need. (declare-fun TestFunc (Int Bool Int) Int). But when I use a define-fun, this (define-fun Main@main ((n Int)) (Int) .... is not available to access with m.get_func_decl(), I suppose some optimization happens that removes the declaration. So, my question is, are there any alternatives to the goal that I have in mind of getting a list of the sorts used in the smt file with no constructors?

Issues with real value calculation in z3

2019-12-02T11:24:26Z

I am working on a problem where I want to learn real parameters based on certain constraints. Following is a snippet of the code:

s = Solver()
def logistic_function(x, y):
   out = y[0]
   for i in range(len(x)):
      out = out + x[i] * y[i + 1]
   return out

self.W = RealVector('w', X.shape[1]+1)
self.F = RealVector('f', X.shape[0])

for h in hard_instances:
  if y[h] == 1:
      self.model.add(Learner.logistic_function(list(X.iloc[h]), self.W) >= 0)         
  else:
      self.model.add(Learner.logistic_function(list(X.iloc[h]), self.W) < 0)         
  self.model.add(Learner.logistic_function(list(X.iloc[h]), self.W) == self.F[h])

s.check()

Where {X,y} is a dataset and hard_instances is a set of indexes that I am working with. After I get a model solution from the z3, I manually calculate the Learner.logistic_function(list(X.iloc[h]), self.W) value for each of the indices in the hard_instance by extracting the W and compare it with the F[h] values. Following are the results for both (with the size of hard_instances being 100):

Confidence value calculated using z3 output:

[-27.378400928361582, -24.54479132404113, -24.307289651276747, -31.70713297755848, -30.762167609027458, -31.315939646075787, -33.00420507718851, -31.744112911331754, -26.23355531746848, -31.36228488104281, -30.427736819536484, -31.50527359981793, -42.88965873739677, -31.707129367228667, -31.56210015506779, -32.12409972766397, -31.70713297755848, -30.031558658483476, -18.358324137431104, -32.05022247782185, -41.531034659230095, -32.29000919967995, -31.75974435910986, -31.663303581555095, -31.492373296661544, -31.31746775645906, -31.707165983877054, -31.347401145915946, -9013.822052472326, -31.75724273178162, -38.284678733394, -290.3139883637738, -38.55432745005057, 186.6069890256151, -44.1131569461781, -3965.3468548458463, -30.19582424657528, -31.81069063619864, -30.619869067329255, -31.58128167212442, -31.822174319008383, -37.18356870531899, -33.442884835165096, -51.320302912234084, -267.50833857889654, -28.402318357266232, -31.62745176425138, 416.1353823972281, -40.42543492186646, -28.541400567435975, -94.80187721209138, -32.013861248574415, -29.42849153859601, -32.14935341971468, -31.20975052479889, 34.2925702396417, -52.91711293409269, -31.772331866138927, -28.05140296433753, -36.58557486365847, -31.83338866474074, -36.5299223283415, -31.327926505869392, -199.5517369747143, -32.08369384912356, -32.07316618164427, -98.62741827618949, -1003.470954079502, -31.240876251803435, 456.34073138747084, -64.27303567782826, -49.714357622299886, -31.905532688175438, 15.611397869700923, 518.5055614575923, -30.65519656405803, -72.45941570859743, -31.967928531880276, -30.55418177994407, -31.225101988980224, -395.9939788509901, -53.142500004465916, -29.61894900393206, -31.756397212326476, -32.51642103656665, -31.12483808710671, -30.768528286960102, -765.2299421009044, 240.09127856915606, 47.958346445463505, -30.42562757004379, -34.02946877293487, 245.48085838630791, -53.48190520867068, -11.398510468740053, -27.119576978335733, -1472.8001539856432, -7.909727924310422, -31.984175109074794, -1246.733548266756]

Values of the F variable:

['6.63397?', '48.31824?', '9.84546?', '-0.5', '0', '0', '-0.5', '-5.38594?', '-0.5', '0', '2.67479?', '-3.55787?', '-10.59216?', '-0.5', '-2.87871?', '-0.5', '-0.5', '-0.5', '21.51906?', '-0.84313?', '0', '-0.5', '-0.5', '-0.5', '-3.33203?', '0', '-0.5', '0', '-8980.16307?', '-0.5', '-7.06012?', '-248.88109?', '-6.90423?', '-0.5', '-12.90605?', '-3945.30152?', '-0.5', '0', '2.09643?', '0.57093?', '-0.5', '0', '-0.5', '-0.5', '-227.57308?', '0', '0', '490.58834?', '-0.5', '0', '-20.46458?', '-0.5', '-0.5', '-0.5', '0', '75.43883?', '-0.5', '-0.5', '3.39666?', '-0.5', '-0.5', '0', '0', '-91.32681?', '-1.13005?', '0', '-41.40830?', '-972.60267?', '0', '-0.5', '0', '0', '-0.5', '43.98384?', '570.67543?', '-0.5', '-41.06592?', '0', '8.24429?', '-3.43914?', '-377.45813?', '-21.85040?', '0', '-11.83317?', '-4.00421?', '-0.5', '0.53349?', '-691.19144?', '264.52677?', '68.84287?', '9.83243?', '3.52497?', '269.78794?', '-21.63869?', '40.52079?', '6.89110?', '-1451.54107?', '26.21240?', '0', '-1190.68525?']

There seems to be a huge difference in the values calculated within z3 (represented by F) and values I calculate based on the solution that I get from z3. These values should be same.

Also, hard_instances are random samples from the full dataset. This kind of discrepancy happens only with some samples. For a lot of the samples, the value I calculate and the value I get from z3 are same. Also, there is no discrepancy if I use the Integer solver and learn integer parameters instead of real ones.

Detecting an unbounded objective in Z3 OCaml API

2025-06-13T19:08:54Z

Is there a way in the OCaml Z3 API to detect, after optimizing a problem and getting a model, to check if the objective was actually unbounded?

One method I see is to add a constraint "I want something bigger than this value I obtained", but that sounds a bit overkill..

Avoiding `unknown` for *, / over Reals?

2025-06-12T12:25:54Z

I'm trying find a solution to a problem of dividing elements from a Sequence into N groups that are roughly evenly distributed. I thought I was making good progress by using a "G-Test" and setting a goal of it being under some maximum value, but I keep getting "unknown" and I think I narrowed it down to this (ln-approx x) function. Since z3 can't do (ln x) I am hoping to use this approximation, but even when avoiding x = -1 I don't see success. I get unknown and a reason of canceled.

Is there a way to avoid this unknown?

Is there a better technique for evaluating a solutions "cardinal balance" among partitions, I might call it?

; approximation that looks close enough for me on the graph for [0 .. 1]
(define-fun ln-approx ((x Real)) Real (ite (<= 0.0 x 1.0) (* 2.0 (/ (- x 1.0) (+ x 1.0))) 1000.0))

By the way, is there a way to write in native z3 to (get-model) only if (check-sat) sat and ask for reasons and other diagnostics if unsat?

Here is the function I'm using instead of ln compared to ln which I assume will be close enough for a useful g-test calculation. Since 0 < O < E, then 0.0 < O/E <= 1.0. The E = 0 case is ited in my g-test implementation.

https://www.desmos.com/calculator/1wh6g3glkx

For background, here's my current g-test implementation, (missing some of the supporting types):

; g-test of an attribute
(define-fun attr-g-test ((attr-count-accessor (Array AttrCounts Int))) Real
    (* 2.0
    (seq.foldli
        (lambda ((group_0_based Int) (half-score Real) (ignored Bool))
            (let 
                ((O (attr-count-accessor (attr-counts students (+ group_0_based 1))))
                (E (attr-count-accessor G_COUNTS)))
                (+ half-score (ite (< 0 O E) (* O (ln-approx (/ O E))) 0.0)))
                ;(+ half-score (* O 1.2))) ;; something like this instead is `sat` (but otherwise useless)
        )
        0 ; offset
        0.0 ; null-hypothesis initial value
        group-iterable-range))
)

How to represent logarithmic formula in z3py

2016-07-27T06:48:02Z

I am very new to z3py. I am trying to code the following logarithmic expressions in z3py .

log(x,y)

I did search stack overflow a lot and came across a similar question, but unfortunately I could not get a satisfactory enough answer. Please help me!

Maximizing nth largest element of grid

2023-05-03T01:39:07Z

I've got a numpy array (48 x 3) of IntVectors (X) where various subsections of this array have constraints. I also have a (48 x 1) of pre-defined integer constants (initial_scores).

Given these constraints I'd like to maximize for the 13th largest possible row-sum; that is if we took [initial_scores[k] + X[k, 0] + X[k, 1] + X[k, 2] for k in range(48)], sorted it (descending) and returned the 13th element.

In some literature I came across the nth and a mk_seq_nth function but neither are defined functions so I'm likely not using them correctly, or perhaps they're not available in z3py?

Here's a gist of the code (69 LOC).

Record usage in Z3 especially with Arrays (Sets) and uninterpreted field constants

2025-06-10T14:20:21Z

I have a few noob questions regarding usage and style in z3 (smt syntax directly). I don't have a theoretical background on solvers, but I would still like to be able to take advantage of the neatness of Z3 without needing to deeply understand the theory (that's fair, no?).

Sample problem: I want to assign Students to distinct Seats. The Seats have letter names because I think that's simpler to write in SMT than if they were numbered. The Student type only has a name and seat field so far, but please consider that the Students might get several more fields and additional seating constraints in the future.

(declare-datatypes () ((Seat A B C D E F G)))

(declare-datatypes () ((Student (mkstudent (name String) (seat Seat)))))

(declare-const S001 Student)
(declare-const S002 Student)

(assert (= (name S001) "Alice"))
(assert (= (name S002) "Bob"))

(assert (forall ((l Student) (r Student)) (xor (= l r) (distinct (seat l) (seat r)))))
; (assert (forall ((l Student) (r Student)) (implies (distinct l r) (distinct (seat l) (seat r))))) ; doesn't work either
(check-sat)
;(get-model)

This is Unsat currently. Why? I think I'm saying that "For all pairs of known Students that exist, either the student is paired with itself XOR the compared students are in distinct seats." But I might be saying "For all pairs of imaginable Students .."

If its the later, do I need to express the set of students as an array and forall over their indexes? Or is there a more natural way to say it?

It feels awkward to have to declare S001, S002 and then assert each field independently. If using an array is correct anyway, I'd rather say something like:

(declare-datatypes () ((Seat A B C D E F G)))

(declare-datatypes () ((Student (mkstudent (name String) (seat Seat)))))

(declare-const students [
    (mkstudent "Alice" _)
    (mkstudent "Bob" _)
])

where there is some placeholder (an uninterpreted constraint?) for the seat field. But I cannot figure out how to leave that free anonymously. And I don't know if there's such a syntax for arrays.

The only way I can get close to this is by pre-declaring a named Seat for each Student and using that in the constructor, but this feels really awful ergonomically - and therefore feels like I'm just doing it wrong. Like, what would be the point of a Record if we have to declare unique identifiers for the instance fields anyway?? Especially presuming that I wouldn't ever have to mention those identifiers again since there are other Record-accessors to get at them. Sure, I could assert (= (name (select students 0)) "Alice") leaving the seat field unconstrained, but as my Student type grows with new valued-fields, this would get ugly and then it makes constructors not so useful.

(declare-const SeatAlice Seat)
(declare-const SeatBob Seat)

(declare-const students (Array Int Student))
(assert (= (select students 0) (mkstudent "Alice" SeatAlice)))
(assert (= (select students 1) (mkstudent "Bob" SeatBob)))

I'm not finding any documentation on how to use arrays and records and constructors and uninterpreted constraints all together. Just minimal examples of them independently, at best.

Many of my questions here are syntax-related - and maybe SMT/Z3 language just isn't prioritizing ergonomics and that is important to know - but again I'm checking with you here because maybe the awkwardness is a signal that I'm just doing it wrong and that there's a much more elegant way that is more readable and possibly even better for Z3 itself.

Updates

This feels a little better using sequence instead of array.

(declare-datatypes () ((Seat A B C D E F G)))
(declare-datatypes () ((Student (mk-student-ctor (fname String) (lname String) (seat Seat)))))

(define-fun mk-student ((fname String) (lname String)) Student
    ((declare-const s Seat)
    (mk-student-ctor fname lname s))
)

;; (define-fun mk-student ((fname String) (lname String)) Student
;;     ; doesn't work, but how could (define-const s Seat) be used in an expression as a local?
;;     (let ((s Seat))
;;     (mk-student-ctor fname lname s))
;; )

(declare-const students (Seq Student))

(assert (= students (seq.++ 
    (seq.unit (mk-student "Alice" "Smith")) 
    (seq.unit (mk-student "Bob" "Baker"))
    ; ...
)))

But I still can't figure out how to encapsulate the concept of an uninterpreted seat field in a constructed Student. Because declare-const is a command, I don't know how it could be used in an expression or if there is an alternative syntax for declaring a const locally (or inline). And in a define-fun, I don't see any way to make a Student without the constructor function which requires all arguments and thus I cannot even resign to constraining the fields one-at-a-time in my new mk_student() factory.

Z3-Solver (z3.z3types.Z3Exception: Z3 invalid substitution, expression pairs expected.)

2024-03-12T09:54:59Z

I have a relative complex Z3 boolean formula and when trying to set the values of a particular variable , I get the following error :
raise Z3Exception(msg) z3.z3types.Z3Exception: Z3 invalid substitution, expression pairs expected.

I tried the following :


def create_z3_formula_bdd(dimacs_file):
    variable_names = {
        1: 'inflow1', 2: "inflow1'",
        3: 'inflow2', 4: "inflow2'",
        5: 'level@0.3.107', 6: "level@0.3.107'",
        7: 'level@1', 8: "level@1'",
        9: 'level@2', 10: "level@2'",
        11: 'level@3', 12: "level@3'",
        13: 'level@4', 14: "level@4'",
        15: 'level@5', 16: "level@5'",
        17: 'level@6', 18: "level@6'",
        19: 'outflow', 20: "outflow'",
        21: '_jx_b0'
    }
    with open(dimacs_file, 'r') as f:
        dimacs_lines = f.readlines()

    # Parse variables and clauses
    variables = set()
    clauses = []
    for line in dimacs_lines:
        tokens = line.split()
        if tokens[0] == 'p':
            num_vars = int(tokens[2])
        elif tokens[0] != 'c' and tokens[0] != '0':
            clause = [int(var) for var in tokens[:-1]]
            variables.update(map(abs, clause))
            clauses.append(clause)

    z3_variables = {var: Bool(variable_names[abs(var)]) for var in variables}

    # Create Z3 clauses
    z3_clauses = [Or([z3_variables[abs(literal)] if literal > 0 else Not(z3_variables[abs(literal)]) for literal in clause]) for clause in clauses]

    return And(z3_clauses)

 formula_bdd = create_z3_formula_bdd('neg_water_reservoir.cnf')
 substitution_map = {variable_names[1]: False}
 formula_with_substitution = substitute(formula_bdd, substitution_map)

Modular arithmetic using z3

2021-03-24T12:35:13Z

I'm trying to prove statements such as the following:

(assert (=
    (mod i n)
    (mod j n)))

(assert (> n 0))
    
(assert (not (=
    (mod (+ i 1) n)
    (mod (+ j 1) n))))

(check-sat)
(get-model)

Others are:

(((i % n) + j) % n) == ((i + j) % n)
((i - n + 1) % n) == ((i + 1) % n)
((((a - 1) % n) + 1) % n) == (a % n)

But z3 does not seem to terminate when proving these statements. Are they beyond the power of z3/smt solvers?

If it is the only way I would not mind doing more explicit proof steps, but these rules seem so elementary I would not know where to begin. Even when using induction I quickly run into cases (like the initial example) that I would expect to be true, but which do not seem to be provable with z3.

I am using z3 4.8.6, for what it's worth. Can anyone shed some light on this why this is hard, or maybe point me in the direction of papers/z3 flags that make this feasible?

Which version of Z3 does VeriEQL use?

2025-05-29T16:08:19Z

I am trying to set up VeriEQL on my computer (Ubunty, Python 3.10) from this repository: https://github.com/VeriEQL/VeriEQL

However, when I run python __main__.py I get error message:

 File "/mnt/compression/VeriEQL/constants.py", line 33, in <lambda>
    And = lambda *args: Z3_And(*args, ctx=Z3_CONTEXT)
TypeError: And() got an unexpected keyword argument 'ctx'

I tried installing the following versions of z3 via pip install:

z3-solver-4.5.1.0
z3-solver-4.11.2.0
z3-solver-4.8.12.0
z3-solver-4.15.0.0

but the error persists.

And I do not know to to print z3 version from __main__.py to make sure that the installed version is indeed loaded.

Z3py: how to get the list of variables from a formula?

2012-12-29T09:34:17Z

In Z3Py, I have a formula. How can I retrieve the list of variables using in the formula?

Z3 Sudoku Solver

2014-05-04T00:47:15Z

I was on the site rise4fun a few weeks ago and they had a python code that converted a sudoku puzzle input file to z3. I checked again today and the file is gone, and was wondering if anyone had this code or could explain to me how to implement it. Thanks!!

`div` versus `/` in SMTLIB

2025-04-04T14:52:33Z

can someone explain the difference between / and div in SMTLIB? My impression is that the former was for Real division and the latter for Int division. Concretely I find that if I write

(define-fun SMTLIB_OP_DIV ((x Int) (y Int)) Int (/ x y))

Then both z3 and cvc5 will complain about the above.

However I also find that if I have the following query

(declare-const a Int)
(declare-const b Int)

(assert (>= b 32))
(assert (= a (/ b 8)))  
(assert (not (= (/ b a) 8))) 
(check-sat)

Then both cvc5 and z3 will say unsat but if I replace the / with div

(declare-const a Int)
(declare-const b Int)

(assert (>= b 32))
(assert (= a (div b 8)))  
(assert (not (= (div b a) 8))) 
(check-sat)

Then they both say sat (!)

Can someone explain? My hunch is there is some internal coercion going on perhaps? But then why wouldn't I just always use / and why is the coercion disallowed in the define-fun?