CODEWITHSUNDEEP
javaz3smt
Boris
Boris

Reputation: 371

Z3 - try-for causes segmentation faults

I am using the Java-API to communicate with Z3 on Ubuntu Linux 14.04. Regarding Z3, I use the current version of the master-branch found on github (compiled today).

The basic structure of the formulas, for which I want to check satisfiability, is as follows:

(and (exists ((x1 S1) ... (xn Sn)) p(x1,...,xn)) 
     (not (exists ((x1 S1) ... (xm Sm)) q(x1,...,xm))))

where the Si may be Bool, an enumeration Sort, Real or Integer and p and q are formulas containing:

However, the formulas may either contain integers or reals but not both.

In order to check satisfiability I create a solver using the tactic:

(or-else (try-for smt x) (then qe smt))

The reason is that some formulas are simple and therefore fast to check and do not require quantifier elimination, but the plain smt solver fails for some without quantifier elimination. Since it may take very long for the smt solver to fail, I use try-for with a timeout of x.

Now the problem is that depending on the value of x this tactic produces segmentation faults after a few hundred satisfiability checks (the actual number varies). I have also observed that larger values tend to be safer, but this depends on the complexity of the formulas p and q. Currently, I am using values in the range from 70 to 200.

Since the actual number of satisfiability checks necessary to reproduce the problem varies, I cannot give a concrete minimal example triggering the problem.

My question is: Should low timeout values generally be avoided or is there a way to work around this problem? I.e. is it possible to use a timeout of 70 ms and to try quantifier elimination afterwards?

Another question: Is there a more efficient tactic for the kind of problem I described, considering that I do not need a model in most cases? Or would it be necessary to give more details?

EDIT: I just realized that the combination with try-for actually produces wrong results in some cases, but only after certain number of satisfiability checks, regardless of the actual value of x (Z3 @ rise4fun produces the correct result). A solver using this tactic deemed an unsatisfiable formula to be satisfiable, while the tactic (then qe smt) produced the correct result. Link to check of formula producing the correct result

Upvotes: 3

Views: 209

Answers (1)

Boris
Boris

Reputation: 371

As indicated in a comment, the issue is now resolved thank to a bugfix by the Z3-team (closed bug report). This bugfix was integrated in the next released version, Version 4.4.1, which at the timing of writing is the latest.

Upvotes: 0

Related Questions