Hi, on the following formula Z3 leaks memory.
(declare-fun skoY () Real)
(declare-fun skoX () Real)
(declare-fun pi () Real)
(assert (= true (= (- (+ skoY (+ (+ 900000000000000000000000 (* skoX (- 900000000)))
(- (* skoY (* skoY (* skoY (* skoY (* skoY (- skoY (+ skoY
(* skoY (* skoY (* skoX (* skoX (/ (- 15625) 4158))))))))))))))))
(+ 1800060000000000000000000 (* skoX (* skoX 1800060000))))
(and (<= 100 skoX) (and (not (<= 0 pi)) (not (<= pi 0))))))
(check-sat)
The original formula came from the SMTLIB benchmark suite and already contained these huge numbers.
unsat
ast_manager LEAKED: 6
Leaked: bv[4:4]
id: 475
Leaked: bv[2:3]
id: 464
OS: Ubuntu 18.04
Revision: ebb7d60
Hi, on the following formula Z3 leaks memory.
The original formula came from the SMTLIB benchmark suite and already contained these huge numbers.
OS: Ubuntu 18.04
Revision: ebb7d60