### Z3Py Encoding of Install Problem Example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-programming/02 - Z3 Python - Readonly/01 - Introduction.md

An example demonstrating how to encode the install problem using Z3Py, including DependsOn and Conflict functions, boolean variables, and the solve function.

```z3-py
def DependsOn(pack, deps):
    return And([ Implies(pack, dep) for dep in deps ])

def Conflict(p1, p2):
    return Or(Not(p1), Not(p2))

a, b, c, d, e, f, g, z = Bools('a b c d e f g z')

solve(DependsOn(a, [b, c, z]),
      DependsOn(b, [d]),
      DependsOn(c, [Or(d, e), Or(f, g)]),
      Conflict(d, e),
      a, z)
```

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

### Installation

Source: https://github.com/microsoft/z3guide/blob/main/website/README.md

Commands to install dependencies for the website.

```sh
$ npm install 
$ yarn
```

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

### Install Dependencies

Source: https://github.com/microsoft/z3guide/blob/main/README.md

Installs project dependencies using Yarn.

```bash
yarn
```

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

### Basic Datalog Example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-programming/02 - Z3 Python - Readonly/04 - Fixedpoints.md

Illustrates declaring relations, rules, and posing queries in the Datalog engine.

```z3-python
fp = Fixedpoint()

a, b, c = Bools('a b c')

fp.register_relation(a.decl(), b.decl(), c.decl())
fp.rule(a,b)
fp.rule(b,c)
fp.set(engine='datalog')

print ("current set of rules\n", fp)
print (fp.query(a))

fp.fact(c)
print ("updated set of rules\n", fp)
print (fp.query(a))
print (fp.get_answer())
```

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

### reduce-args example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/03 - strategies/06 - summary.md

Example demonstrating the use of the reduce-args tactic.

```z3
(declare-fun f (Int Int) Bool)
(declare-const x Int)
(assert (f 1 2))
(assert (f 1 3))
(assert (f 2 4))
(assert (f 2 5))
(assert (f 1 6))
(assert (f 1 7))
(assert (f 1 x))
(apply reduce-args)
```

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

### Basic Datalog Example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/05 - fixedpoints/05 - syntax.md

An example of a program in the BDDBDDB format for comparing benchmarks.

```datalog
Z 64

P0(x: Z) input
Gt0(x : Z, y : Z) input
R(x : Z) printtuples
S(x : Z) printtuples
Gt(x : Z, y : Z) printtuples
Gt(x,y) :- Gt0(x,y).
Gt(x,y) :- Gt(x,z), Gt(z,y).
R(x) :- Gt(x,_).
S(x) :- Gt(x,x0), Gt0(x,y), Gt0(y,z), P0(z).
Gt0("a","b").
Gt0("b","c").
Gt0("c","d").
Gt0("a1","b").
Gt0("b","a1").
Gt0("d","d1").
Gt0("d1","d").
P0("a1").
```

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

### Diff-neq Solver Example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/03 - strategies/06 - summary.md

Example for the diff-neq solver for integer problems.

```z3
(declare-const x Int)
(declare-const y Int)
(assert (<= 0 x))
(assert (<= x 1))
(assert (<= 0 y))
(assert (<= y 1))
(assert (not (= (+ x (* -1 y)) -1)))
(assert (not (= (+ x (* -1 y)) 1)))
(assert (not (= (+ x (* -1 y)) 0)))
(apply diff-neq)
```

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

### reduce-bv-size example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/03 - strategies/06 - summary.md

Example demonstrating the use of the reduce-bv-size tactic.

```z3
(declare-const x (_ BitVec 32))
(assert (bvsle (bvneg (_ bv2 32)) x))
(assert (bvsle x (_ bv2 32)))
(assert (= (bvmul x x) (_ bv9 32)))
(apply (and-then simplify reduce-bv-size))
```

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

### Quasi-macro-finder Example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/03 - strategies/06 - summary.md

An example demonstrating the use of the quasi-macro-finder tactic in Z3.

```z3
(declare-fun f (Int Int Int) Int)
(declare-fun p (Int) Bool)
(declare-const a Int)

(assert (forall ((x Int) (y Int)) (= (f x y 1) (* 2 x y))))
(assert (p (f 8 a (+ a 8))))
(apply quasi-macros)
```

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

### sat-preprocess example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/03 - strategies/06 - summary.md

Example demonstrating the use of the sat-preprocess tactic.

```z3
(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(declare-const d Bool)
(declare-const e Bool)
(declare-const f Bool)
(declare-fun p (Bool) Bool)
(assert (=> a b))
(assert (=> b c))
(assert a)
(assert (not c))
(apply sat-preprocess)
```

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

### Install z3-solver

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-programming/02 - Z3 Python - Readonly/01 - Introduction.md

Command to install the z3-solver package using pip.

```bash
pip install z3-solver
```

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

### Install Yarn

Source: https://github.com/microsoft/z3guide/blob/main/README.md

Installs Yarn globally if it's not already installed.

```bash
npm install -g yarn
```

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

### normalize-bounds Example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/03 - strategies/06 - summary.md

Example demonstrating the use of the normalize-bounds tactic.

```z3
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (<= 3 x))
(assert (<= (+ x y) z))
(apply normalize-bounds)
```

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

### Basic Solver API Demonstration

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-programming/02 - Z3 Python - Readonly/01 - Introduction.md

Demonstrates the creation of a solver, adding constraints, checking satisfiability, and using push/pop for scope management.

```z3-py
x = Int('x')
y = Int('y')

s = Solver()
print (s)

s.add(x > 10, y == x + 2)
print (s)
print ("Solving constraints in the solver s ...")
print (s.check())

print ("Create a new scope...")
s.push()
s.add(y < 11)
print (s)
print ("Solving updated set of constraints...")
print (s.check())

print ("Restoring state...")
s.pop()
print (s)
print ("Solving restored set of constraints...")
print (s.check())
```

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

### Difference Arithmetic Example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/02 - theories/01 - Arithmetic.md

An example demonstrating difference arithmetic constraints, often used in job-shop scheduling, modeling task start times, durations, and non-overlap conditions.

```z3
(set-logic QF_IDL) ; optional in Z3
(declare-fun t11 () Int)
(declare-fun t12 () Int)
(declare-fun t21 () Int)
(declare-fun t22 () Int)
(declare-fun t31 () Int)
(declare-fun t32 () Int)

(assert (and (>= t11 0) (>= t12 (+ t11 2)) (<= (+ t12 1) 8)))
(assert (and (>= t21 0) (>= t22 (+ t21 3)) (<= (+ t22 1) 8)))
(assert (and (>= t31 0) (>= t32 (+ t31 2)) (<= (+ t32 3) 8)))
(assert (or (>= t11 (+ t21 3)) (>= t21 (+ t11 2))))
(assert (or (>= t11 (+ t31 2)) (>= t31 (+ t11 2))))
(assert (or (>= t21 (+ t31 2)) (>= t31 (+ t21 3))))
(assert (or (>= t12 (+ t22 1)) (>= t22 (+ t12 1))))
(assert (or (>= t12 (+ t32 3)) (>= t32 (+ t12 1))))
(assert (or (>= t22 (+ t32 3)) (>= t32 (+ t22 1))))
(check-sat)
(get-model)
```

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

### Datalog with Explanations

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-programming/02 - Z3 Python - Readonly/04 - Fixedpoints.md

Demonstrates how to get an explanation for a derived query in the Datalog engine.

```z3-python
fp = Fixedpoint()

a, b, c = Bools('a b c')

fp.register_relation(a.decl(), b.decl(), c.decl())
fp.rule(a,b)
fp.rule(b,c)
fp.fact(c)
fp.set("datalog.generate_explanations", True)
fp.set(engine='datalog')
print (fp.query(a))
print (fp.get_answer())
```

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

### Relations with Arguments Example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-programming/02 - Z3 Python - Readonly/04 - Fixedpoints.md

Illustrates relations with arguments using edges and paths in a graph.

```z3-python
fp = Fixedpoint()
fp.set(engine='datalog')

s = BitVecSort(3)
edge = Function('edge', s, s, BoolSort())
path = Function('path', s, s, BoolSort())
a = Const('a',s)
b = Const('b',s)
c = Const('c',s)

fp.register_relation(path,edge)
fp.declare_var(a,b,c)
fp.rule(path(a,b), edge(a,b))
fp.rule(path(a,c), [edge(a,b),path(b,c)])

v1 = BitVecVal(1,s)
v2 = BitVecVal(2,s)
v3 = BitVecVal(3,s)
v4 = BitVecVal(4,s)

fp.fact(edge(v1,v2))
fp.fact(edge(v1,v3))
fp.fact(edge(v2,v4))

print ("current set of rules", fp)


print (fp.query(path(v1,v4)), "yes we can reach v4 from v1")

print (fp.query(path(v3,v4)), "no we cannot reach v4 from v3")
```

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

### Launch Docs Server

Source: https://github.com/microsoft/z3guide/blob/main/README.md

Clears the cache and starts the development server for hot reloading.

```bash
yarn clear; # for clearing cache
yarn start;
```

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

### Tactics

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/03 - strategies/03 - tactics.md

This example shows how to use tactics in Z3.

```smtlib
(assert (= y (bvadd z z)))

(check-sat-using 
 (par-or
  ;; Strategy 1: use bit-blasting
  (then simplify bit-blast sat)
  ;; Strategy 2: use default solver
  smt))

(get-model)

(echo "using different random seeds...")

(check-sat-using
 (par-or
  ;; Strategy 1: using seed 1
  (using-params smt :random-seed 1)
  ;; Strategy 1: using seed 2
  (using-params smt :random-seed 2)
  ;; Strategy 1: using seed 3
  (using-params smt :random-seed 3)))

(get-model)
```

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

### Demonstrating tactic combinators

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-programming/02 - Z3 Python - Readonly/03 - Strategies.md

This example demonstrates the usage of 'Repeat' and 'OrElse' combinators with 'split-clause' tactic.

```z3-python
x, y, z = Reals('x y z')
g = Goal()
g.add(Or(x == 0, x == 1), 
      Or(y == 0, y == 1),
      Or(z == 0, z == 1),
      x + y + z > 2)

# Split all clauses"
split_all = Repeat(OrElse(Tactic('split-clause'),
                          Tactic('skip')))
print (split_all(g))

split_at_most_2 = Repeat(OrElse(Tactic('split-clause'),
                          Tactic('skip')),
                         1)
print (split_at_most_2(g))
```

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

### Recursive Function Definition

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/01 - logic/07 - Recursive Functions.md

Example of defining recursive functions 'length' and 'nat-list' and asserting properties about them.

```z3
(define-fun-rec length ((ls (List Int))) Int
   (if ((_ is nil) ls) 0 (+ 1 (length (tail ls)))))

(define-fun-rec nat-list ((ls (List Int))) Bool 
   (if ((_ is nil) ls)
       true
       (and (>= (head ls) 0) (nat-list (tail ls)))))

(declare-const list1 (List Int))
(declare-const list2 (List Int))
(assert (> (length list1) (length list2)))
(assert (not (nat-list list2)))
(assert (nat-list list1))
(check-sat)
(get-model)
```

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

### Build Documentation

Source: https://github.com/microsoft/z3guide/blob/main/README.md

Clears the cache and builds the documentation for server-side rendering.

```bash
yarn clear; # clearing your cache first is always recommended
yarn build;
```

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

### Using FailIf with Probes

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-programming/02 - Z3 Python - Readonly/03 - Strategies.md

An example showing how to build a tactic using FailIf and apply a probe directly to a goal.

```z3-python
x, y, z = Reals('x y z')
g = Goal()
g.add(x + y + z > 0)

p = Probe('num-consts')
print ("num-consts:", p(g))

t = FailIf(p > 2)
try:
    t(g)
except Z3Exception:
    print ("tactic failed")

print ("trying again...")
g = Goal()
g.add(x + y > 0)
print (t(g))
```

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

### Serve Built Documentation

Source: https://github.com/microsoft/z3guide/blob/main/README.md

Serves the built documentation files without hot-reloading.

```bash
yarn serve
```

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

### Using the split-clause tactic

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-programming/02 - Z3 Python - Readonly/03 - Strategies.md

This example shows how to use the 'split-clause' tactic to break down a goal into subgoals based on clauses.

```z3-python
x, y = Reals('x y')
g  = Goal()
g.add(Or(x < 0, x > 0), x == y + 1, y < 0)

t = Tactic('split-clause')
r = t(g)
for g in r: 
    print(g)
```

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

### pb2bv Example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/03 - strategies/06 - summary.md

Example demonstrating the conversion of pseudo-boolean constraints to bit-vectors using the pb2bv tactic.

```z3
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const u Int)
(assert (<= 0 x))
(assert (<= 0 y))
(assert (<= 0 z))
(assert (<= 0 u))
(assert (<= x 1))
(assert (<= y 1))
(assert (<= z 1))
(assert (<= u 1))
(assert (>= (+ (* 3 x) (* 2 y) (* 2 z) (* 2 u)) 4))
(apply pb2bv)
```

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

### Mutually Recursive Functions Definition

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/01 - logic/07 - Recursive Functions.md

Example of defining mutually recursive functions 'ping' and 'pong' and asserting properties.

```z3
(define-funs-rec 
   ((ping ((x Int) (y Bool)) Int)
    (pong ((a Int) (b Bool)) Int))

   ((if y (pong (+ x 1) (not y)) (- x 1))
    (if b (ping (- a 1) (not b)) a)))

(declare-const x Int)
(assert (> x 0))
(assert (> (ping x true) x))
(check-sat)
(get-model)
```

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

### Testing Website Command

Source: https://github.com/microsoft/z3guide/blob/main/README.md

Command to start the local development server for testing the website.

```bash
yarn start
```

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

### Combining simplify and solve-eqs tactics

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-programming/02 - Z3 Python - Readonly/03 - Strategies.md

This example demonstrates creating a tactic by composing 'simplify' and 'solve-eqs' using the 'Then' combinator.

```z3-python
x, y = Reals('x y')
g  = Goal()
g.add(x > 0, y > 0, x == y + 2)
print (g)

t1 = Tactic('simplify')
t2 = Tactic('solve-eqs')
t  = Then(t1, t2)
print (t(g))
```

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

### Fixedpoint Solver Example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-programming/02 - Z3 Python - Readonly/04 - Fixedpoints.md

This code snippet demonstrates the usage of Z3's fixedpoint solver to define relations, rules, and query for a fixedpoint.

```python
from z3 import *

Expr = Datatype('Expr')
Expr.declare('Max')
Expr.declare('f')
Expr.declare('I', ('i', IntSort()))
Expr.declare('App', ('fn',Expr),('arg',Expr))
Expr = Expr.create()
Max  = Expr.Max
I    = Expr.I
App  = Expr.App
f    = Expr.f
Eval = Function('Eval',Expr,Expr,Expr,BoolSort())

x   = Const('x',Expr)
y   = Const('y',Expr)
z   = Const('z',Expr)
r1  = Const('r1',Expr)
r2  = Const('r2',Expr)
max = Const('max',Expr)
xi  = Const('xi',IntSort())
yi  = Const('yi',IntSort())

fp = Fixedpoint()
fp.register_relation(Eval)
fp.declare_var(x,y,z,r1,r2,max,xi,yi)

# Max max x y z = max (max x y) z
fp.rule(
    Eval(App(App(App(Max, max), x), y), z, r2),
    [Eval(App(max, x), y, r1), Eval(App(max, r1), z, r2)],
)

# f x y = x if x >= y
# f x y = y if x < y
fp.rule(Eval(App(f,I(xi)),I(yi),I(xi)),xi >= yi)
fp.rule(Eval(App(f,I(xi)),I(yi),I(yi)),xi < yi)

print(fp.query(And(
    Eval(App(App(App(Max, f), x), y), z, r1),
    Eval(App(f, x), r1, r2), r1 != r2
)))
print (fp.get_answer())
```

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

### Local Development

Source: https://github.com/microsoft/z3guide/blob/main/website/README.md

Command to start the local development server.

```sh
$ yarn start
```

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

### Functional Program Verification Snippet

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-programming/02 - Z3 Python - Readonly/04 - Fixedpoints.md

This snippet shows the beginning of a Z3 Python code example for verifying properties of functional programs, using algebraic data-types to encode closures.

```z3-python
# let max max2 x y z = max2 (max2 x y) z
# let f x y = if x > y then x else y

```

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

### Using Scopes with Push and Pop

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/01 - logic/02 - basiccommands.md

This example demonstrates the use of push and pop commands to manage scopes for assertions and declarations. It includes a case that would result in an error if a declaration is popped before being used.

```z3
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(push)
(assert (= (+ x y) 10))
(assert (= (+ x (* 2 y)) 20))
(check-sat)
(pop) ; remove the two assertions
(push) 
(assert (= (+ (* 3 x) y) 10))
(assert (= (+ (* 2 x) (* 2 y)) 21))
(check-sat)
(declare-const p Bool)
(pop)
(assert p) ; error, since declaration of p was removed from the stack
```

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

### Using the User Propagator Example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-programming/03 - Example Programs/02 - User Propagator.md

This snippet demonstrates the setup and usage of the User Propagator. It initializes a Solver and a TC (Transitive Closure) object, adds relations from `leSortTable` and `leSortSyntaxTable`, adds formulas `fmls`, and then checks for satisfiability.

```z3-python
s = Solver()
b = TC(s)

for (a,b) in leSortTable:
    s.add(leSort(a(),b()))
for (a,b) in leSortSyntaxTable:
    s.add(leSortSyntax(a(), b()))
    
s.add(fmls)
print(s.check())

```

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

### Configuration Options

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/01 - logic/02 - basiccommands.md

Demonstrates the use of set-option and reset commands to configure Z3's behavior, including setting options before and after assertions and resets.

```z3
(set-option :print-success true)
(set-option :produce-unsat-cores true) ; enable generation of unsat cores
(set-option :produce-models true) ; enable model generation
(set-option :produce-proofs true) ; enable proof generation
(declare-const x Int)
(assert (= x 1))
(set-option :produce-proofs false) ; error, cannot change this option after an assertion
(echo "before reset")
(reset)
(set-option :produce-proofs false) ; ok
```

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

### Warmup Example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-programming/01 - Z3 JavaScript Examples.md

A basic example demonstrating Z3.js for propositional logic, showing a formula that establishes there is no number both above 9 and below 10.

```z3-js
const x = Z3.Int.const('x');
Z3.solve(Z3.And(x.ge(10), x.le(9)));
```

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

### Quantifier Example 1

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/01 - logic/05 - Quantifiers.md

An example of a quantifier in SMT-LIB.

```smtlib
(forall ((?U Action) (?V Action)) (implies (= (action2int ?U) (action2int ?V)) (= ?U ?V))))
```

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

### Integer Encoding for VM Placement

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/04 - optimization/06 - asmallcasestudy.md

This Z3 code snippet presents an integer encoding for the virtual machine placement problem, offering a more natural representation for arithmetic constraints.

```z3
(declare-const x11 Int)
(declare-const x12 Int)
(declare-const x13 Int)
(declare-const x21 Int)
(declare-const x22 Int)
(declare-const x23 Int)
(declare-const x31 Int)
(declare-const x32 Int)
(declare-const x33 Int)

(declare-const y1 Int)
(declare-const y2 Int)
(declare-const y3 Int)

(assert (and (>= x11 0) (>= x12 0) (>= x13 0) 
             (>= x21 0) (>= x22 0) (>= x23 0)
             (>= x31 0) (>= x32 0) (>= x33 0)))
             
(assert (and (<= y1 1) (<= y2 1) (<= y3 1)))

(assert (= (+ x11 x12 x13) 1))
(assert (= (+ x21 x22 x23) 1))
(assert (= (+ x31 x32 x33) 1))

(assert (and (>= y1 x11) (>= y1 x21) (>= y1 x31)))
(assert (and (>= y2 x12) (>= y2 x22) (>= y2 x32)))
(assert (and (>= y3 x13) (>= y3 x23) (>= y3 x33)))

(assert (<= (+ (* 100 x11) (* 50 x21) (* 15 x31)) (* 100 y1)))
(assert (<= (+ (* 100 x12) (* 50 x22) (* 15 x32)) (* 75 y2)))             
(assert (<= (+ (* 100 x13) (* 50 x23) (* 15 x33)) (* 200 y3)))

(minimize (+ y1 y2 y3))
(minimize (+ (* 10 y1) (* 5 y2) (* 20 y3)))

;(set-option :opt.priority pareto)
(check-sat)
(get-model)
(get-objectives)

```

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

### Pure SMT-LIB2 Example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/05 - fixedpoints/05 - syntax.md

An example of a Constrained Horn clause satisfiability problem expressed in SMT-LIB2.

```z3
(set-logic HORN)
(declare-fun mc (Int Int) Bool)

(assert (forall ((m Int)) (=> (> m 100) (mc m (- m 10)))))
(assert (forall ((m Int) (n Int) (p Int)) 
           (=> (and (<= m 100) (mc (+ m 11) p) (mc p n)) (mc m n))))

(assert (forall ((m Int) (n Int))
       (=> (and (mc m n) (<= m 101)) (= n 91))))
(check-sat)
(get-model)
```

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

### Basic Constraint Solving

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-programming/02 - Z3 Python - Readonly/01 - Introduction.md

Demonstrates creating integer variables and solving a system of linear constraints.

```z3-py
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)
```

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

### solve-eqs Example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/03 - strategies/06 - summary.md

An example demonstrating the use of the 'solve-eqs' tactic to solve for variables in a given assertion.

```smtlib
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const u Int)
(assert (or (and (= x (+ 5 y)) (> u z)) (= y (+ u z))))
(apply solve-eqs)
```

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

### Distribute Forall Example

Source: https://github.com/microsoft/z3guide/blob/main/website/docs-smtlib/03 - strategies/06 - summary.md

Example for distributing forall over conjunctions.

```z3
(declare-const x Int)
  (declare-fun p (Int) Bool)
  (declare-fun q (Int) Bool)
  (assert (forall ((x Int)) (and (p x) (q x))))
  (apply distribute-forall)
```