# Z3 - trying to get segmentation errors

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

The basic structure of the formulas for which I want to test the feasibility is as follows:

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

```

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

• inequalities between the sums of numeric values ​​and constants
• equality between enumeration values ​​and constants
• boolean values ​​and constants.
• their combinations (conjunctions, disjunctions, negations)

However, formulas can contain whole numbers or numbers, but not both.

To test the feasibility, 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 quick to validate and do not require a quantifier exception, but a simple smt-solver does not work for some without quantifier exception. Since smt can take a very long time to solve, I use try-in with x timeout.

Now the problem is that depending on the value of x, this tactic produces segmentation faults after several hundred feasibility checks (actual number varies). I also noticed that higher values ​​are generally safer, but that depends on the complexity of the p and q formulas. I am currently using values ​​between 70 and 200.

Since the actual number of feasibility checks required to reproduce the problem varies, I cannot provide a specific minimal example causing the problem.

My question is, should low timeouts be avoided altogether, or is there a way around this problem? That is, is it possible to use a 70ms timeout and then try to exclude the quantifier?

Another question is, is there a better tactic for the problem I described, given that I don't need a model in most cases? Or would it be necessary to provide more details?

EDIT: I just realized that the try-for combination actually produces wrong results in some cases, but only after a certain number of feasibility checks, regardless of the actual x value (Z3 @ rise4fun gives the correct result). The solver using this tactic considered the unsatisfactory formula doable, and the tactic `(then qe smt)`

gave the correct result. Link to validate the formula that produces the correct result

+3

source to share

As pointed out in the comment, the issue has now been resolved thanks to the Z3 team fix ( closed bug report ). This fix was included in the next released version 4.4.1, which is the latest at the time of writing.

0

source

All Articles