SegFault when using quantifier elimination in Z3

1
votes

I work with Z3 4.3.1 (from master branch) under MacOS X 10.8. I get a segmentation fault on following example:

(declare-const a Int)
(declare-const b Int)

(assert
  (exists ((k Int))
    (and 
     (= (- (* 2 k) a) 0)
     (= (- (* 2 k) b) 0)
    )
  )
)


(check-sat-using qe)

Any idea, on how to fix this problem ?

2
z3

2 Answers

2
votes

I managed to reproduce the bug you described using OSX and Z3 4.3.1. This bug has been fixed and will be available in the next official release. In the meantime, you can use the nightly build for OSX or build Z3 using the unstable (working-in-progress) branch.

The nightly build can be downloaded at: http://z3.codeplex.com/releases. We have to click at the "Planned" link. I wrote some instructions here.

BTW, if we want to check satisfiability, we should use an end-game tactic (such as smt) after qe, like in the example posted by Axel. If we want to inspect the result produced by qe, we should use (apply qe) instead.

0
votes

The following works ok under Windows XP + Z3 4.3.0

(declare-const a Int)
(declare-const b Int)

(assert
  (exists ((k Int))
    (and 
     (= (- (* 2 k) a) 0)
     (= (- (* 2 k) b) 0)
    )
  )
)
(check-sat-using (then qe smt))
(get-model)