Hi,
For this formula,
(set-option :smt.phase_selection 5)
(set-option :smt.threads 10)
(declare-fun a () String)
(assert (distinct (str.len a) 83))
(check-sat)
Z3 nodeterministicly throws out ast_manager LEARKED:
$ z3/build/z3 small.smt2
sat
$ z3/build/z3 small.smt2
ast_manager LEAKED: 3
Leaked: 84
id: 371
ast_manager LEAKED: 3
Leaked: 84
id: 371
ast_manager LEAKED: 3
Leaked: 84
id: 371
ast_manager LEAKED: 3
Leaked: 84
id: 371
sat
$ cat small.smt2
(set-option :smt.phase_selection 5)
(set-option :smt.threads 10)
(declare-fun a () String)
(assert (distinct (str.len a) 83))
(check-sat)
OS: Ubuntu 18.04
Commit: 37bc4a4
Hi,
For this formula,
Z3 nodeterministicly throws out ast_manager LEARKED:
OS: Ubuntu 18.04
Commit: 37bc4a4