I've installed z3-solver package from PyPi in my Python3 environment using Anaconda Prompt ( pip install z3-solver ) and that's it. The package appears in the site-packages/ directory ( the packag...

I'm looking at doing some verification work where I've got regular tree grammars as an underlying theory. Z3 lets you define your own stuff with uninterpreted functions, but that doesn't tend to w...

What's a good way to encode "at least k / at most k of these boolean variables must be true" constraints in Z3, for arbitrary k and number of boolean variables? I'm thinking of casting "at least k...

I want to use a Int vector as an array index. python. array = [12,45,66,34] s= Solver() x = Int('x') s.add(array[x] == 66) so the x should be 2.. how can i do it?

I am trying to retrieve all possible models for some first-order theory using Z3, an SMT solver developed by Microsoft Research. Here is a minimal working example: (declare-const f Bool) (assert (...

In Z3Py, how can I check if equation for given constraints have only one solution? If more than one solution, how can I enumerate them?

I'd like to use Z3 to solve problems that are most naturally expressed in terms of atoms (symbols), sets, predicates, and first order logic. For example (in pseudocode): A = {a1, a2, a3, ...} # A i...

I am trying to express the sum of the range of an unbounded Array in z3. For instance in Python: IntArray = ArraySort(IntSort(), IntSort()) sum = Function('sum', IntArray, IntSort()) ........ ...

I think there's two different relevant cases here: Case 1: I have a set of boolean variables and I want another boolean variable which is true if any of these variables are true. I'm currently doin...

Recently I am learning SMT solver. Although SMT solver is a new concept to me, it reminds me of logic programming, e.g. Prolog and minikanren. So I tried a classic example of logic programming in S...

Let's assume a very simple constraint: solve(x > 0 && x < 5). Can Z3 (or any other SMT solver, or any other automatic technique) compute the minimum and maximum values of (integer)...

I’m using a project where each time you double the number of threads, you add between 40% to 60% overhead. As hyperthreading increases performance to a maximum of 30% this means, the program runs s...

How to setup a Java development environment for the Z3 SMT solver? Note: Written and answered by the author, see Can I answer my own question?.

Is there a way to run Z3 solver from javascript? Or is there a better SMT solver that I can be used in JavaScript?

In an effort to learn Z3 I tried solving one of my favorite Advent of Code problems (a particularly difficult one, 2018 day 23, part 2) using the Haskell bindings sbv. Spoilers in code ahead... mo...

I am trying to use Z3 library from python however it does not work. It gives an error Int is not defined. I installed the z3 module using pip and as you can see, there is no error message thrown w...

In Microsoft Z3, when we try to solve a formula, Z3 always returns the results in the same sequence, when there are two or more satisfiable solutions. Is it possible to get random results from Z3 ...

I am writing to inquire the theory/algorithm behind the Z3 Optimize function, especially for its maximum and minimum function. This seems pretty magic to me. Is it somehow a binary search or so? Ho...

I wrote an application in Haskell that calls Z3 solver to solve constrains with some complex formulas. Thanks to Haskell I can quickly switch the data type I'm working with. When using SBV's AlgRe...

One of the new features in Z3 4.8.1 is parallel solving: A parallel mode is available for select theories, including QF_BV. By setting parallel.enable=true Z3 will spawn a number of worker thre...

I'm going to create an array with fixed size and initialize it with some values. For example, the following C++ code: a[0] = 10; a[1] = 23; a[2] = 27; a[3] = 12; a[4] = 19; a[5] = 31; a[6] = 41; ...

I'm trying to build Z3 on mac os x. Following README file, I just executed autoconf ./configure make to get an error "omp.h" file not found. I copied the omp.h file from /usr/llvm-gcc-4.2/li...

I'm using Z3 to solve the Eight Queens puzzle. I know that each queen can be represented by a single integer in this problem. But, when I represent a queen by two integers as following: from z3 im...

I'm new to Z3 and I was checking the online python tutorial. Then I thought I could check overflow behavior in BitVecs. I wrote this code: x = BitVec('x', 3) y = Int('y') solve(BV2Int(x) == y, ...

I would like to prove properties of expressions involving matrices and vectors (potentially large size, but size is fixed). For example I want to prove that the outcome of an expression is a diag...