Discussions under General

Use this discussion page to provide feedback on code checkins, suggest features, and to ask project questions.

To report a bug, use the Issue Tracker. To ask questions about using Z3, use StackOverflow.

Enconding a transitive closure in Z3 (routing)

first post: zverlov wrote: Hi, I would like to encode a routing problem using z3. So simpli...

latest post: wintersteiger wrote: This discussion board is not in use anymore as Z3 has moved to [Git...

Problem with Z3-Opt and opt.priority box parameter

first post: zverlov wrote: Hey, I get an error in my JRE when i try to optimize a large deplo...

latest post: wintersteiger wrote: This dicussion board is not in use anymore as Z3 has moved to [GitH...

new tactic: partition

first post: dradorf wrote: I should like to suggest a new tactic that partitions a given SMT-p...

latest post: wintersteiger wrote: This dicussion board is not in use anymore as Z3 has moved to [GitH...

How to automatically check Z3 string by using Microsoft.z3.dll

first post: newfut wrote: I have a smt2 string that is stored in a file *.smt2. I use z3.exe ...

latest post: newfut wrote: Thank you, I will try.

z3 basic question (python)

first post: hdarwin wrote: In [1]: from z3 import * In [2]: x = Int('x') In [3]: solve(x < 5...

latest post: wintersteiger wrote: Thanks for your question. Z3 has moved to github and this forum is ...

LINQ Support missing

first post: MovGP0 wrote: Bart De Smet wrote a LINQ to Z3 Adapter back in 2010. While LINQ is...

latest post: RicardoGer wrote: For completeness: See https://github.com/riwickel/Z3.LinqBinding - ...

QF_FPA Push and Pop

first post: kevinclancy wrote: Does QF_FPA support the push and pop commands yet? When I run z3 on...

latest post: wintersteiger wrote: Thanks for the interest in this! The fpa-api branch has been remove...

Z3 Interpolation API in Java not public

first post: j58 wrote: Z3 team, thanks for making a Java binding for Z3. I've found it ver...

latest post: j58 wrote: Thanks for the quick turnaround. If I construct some good small exa...

Implications of licencing agreement?

first post: f1533135 wrote: If I use the Z3 engine to optimize my theorems, does Microsoft have...

latest post: wintersteiger wrote: Sorry for taking a bit of time on this. As you may have seen alread...

Getting UNKNOWN quickly for suspected SAT cases

first post: Heizmann wrote: Our software model checker generates a lot of SMT queries that cont...

latest post: wintersteiger wrote: I have a feeling I've answered this question elsewhere before, if n...