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