opt.dump_models sat.ddfw_search sat.xor.solver Segementation fault

[muchang]

Hi,
For this formula:

(set-option :opt.dump_models true) 
(set-option :sat.ddfw_search true) 
(set-option :sat.xor.solver true) 
(define-fun s1 () Int 67) 
(define-fun s3 () Int 5) 
(declare-fun s0 () Int) 
(declare-fun s13 () Int) 
(define-fun s2 () Bool (<= s0 s1)) 
(define-fun s4 () Bool (>= s0 s3)) 
(define-fun s10 () Bool s4) 
(define-fun s11 () Bool (and s2 s10)) 
(assert s11) 
(assert (= s0 s13)) 
(maximize s13) 
(check-sat) 

Z3 throws out a segmentation fault:

$ ./z3/build/z3 small.smt2 
Segmentation fault
$ cat small.smt2 
(set-option :opt.dump_models true) 
(set-option :sat.ddfw_search true) 
(set-option :sat.xor.solver true) 
(define-fun s1 () Int 67) 
(define-fun s3 () Int 5) 
(declare-fun s0 () Int) 
(declare-fun s13 () Int) 
(define-fun s2 () Bool (<= s0 s1)) 
(define-fun s4 () Bool (>= s0 s3)) 
(define-fun s10 () Bool s4) 
(define-fun s11 () Bool (and s2 s10)) 
(assert s11) 
(assert (= s0 s13)) 
(maximize s13) 
(check-sat)

OS: Ubuntu 18.04
Commit: 65b2037

[rainoftime]

According to #3635,

as I wrote before: ddfw is experimental and not useful to spend time fixing nits.