Hi,
For this formula:
(set-option :smt.core.minimize true)
(set-option :fp.xform.inline_eager false)
(assert (< 0 (sin 0.2) 6.5))
(check-sat-using horn)
Z3 throws out a segmentation fault:
[543] % z3 small.smt2
Segmentation fault
[544] %
[544] % cat small.smt2
(set-option :smt.core.minimize true)
(set-option :fp.xform.inline_eager false)
(assert (< 0 (sin 0.2) 6.5))
(check-sat-using horn)
[545] %
OS: Ubuntu 18.04
Commit: 9e7af79
Hi,
For this formula:
Z3 throws out a segmentation fault:
OS: Ubuntu 18.04
Commit: 9e7af79