Tag: Z3

I used the following code fragment in z3 4.0 to convert the formula to CNF.

(set-logic QF_UF)< br />(
set-option
:produce-models
true
)
; —— snip —– —
;
; declarations,
; and asse