Welcome to z3 Discussions!

[NikolajBjorner]

Welcome!

Z3 is using Discussions as a place to connect users and contributors. We hope that you:

• Ask questions you’re wondering about.
• Participate in responding to questions.
• Share ideas and engage.

The idea is that discussions can complement the issue tracker that is better for handling bug reports and usability problems. On the other hand, discussions may be a place to maintain threads around your inner feelings about filing fuzzbugs, discussing use cases and what existing and missing solver features may be relevant.

To get started, comment below with an introduction of yourself and tell us about what you do with this community.

[aytey]

inner feelings about filing fuzzbugs

😂

[SweetVishnya]

We perform symbolic execution with Z3 inside (QF_BV) to assist fuzzing and find bugs. We are going to provide you with some queries from Sydr (at the beginning of next year), so we will be able to benchmark Z3 on one more application.

[NikolajBjorner]

This is would be very cool. I am trying to convince the authors of Alive2 to extract benchmarks that exercise their bottlenecks.
They set up a server with comparative evaluation so far, but wrestling out benchmarks is another issue.
There are at least three ways to approach this from z3:

1. Print the solver state before check-sat query to a file.
2. Set the parameter option to log all solver interaction as SMTLIB2 commands. The option is solver.smtlib2_log=myfile.smt2.
3. Use the low level logging feature by starting Z3 session with Z3_open_log("myfile.log"). The log should be re-playable using the same version of Z3 (the log does not replay if I update the API functions).

Sometimes the overhead a tool sees is not transparent when dumping benchmarks. For example, Regehr and Lopes changed the timeout handlers to use persistent threads to avoid overhead during thread creation. Their change to z3 should benefit everybody. Furthermore, the Alive2 interface to z3 opts not to use our mainstream C++ wrapper but has to do it on its own.

[SweetVishnya]

We submitted benchmarks to Smt-comp 2021.

[SweetVishnya]

@NikolajBjorner, benchmarks were moved to https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_BV/-/tree/master/20210219-Sydr