; Query 0 -- Type: InitialValues, Instructions: 5562
; Emited by klee::Z3SolverImpl::getConstraintLog()
(set-info :status unknown)
(declare-fun f_ackermann!0 () (_ BitVec 64))
(assert
 (not (not (not (fp.isNaN ((_ to_fp 11 53) f_ackermann!0))))))
(check-sat)
;   OK -- Elapsed: 1.266003e-02
;   Solvable: true
;     f = [1,0,0,0,0,0,0,0]

; Query 1 -- Type: InitialValues, Instructions: 5576
; Emited by klee::Z3SolverImpl::getConstraintLog()
(set-info :status unknown)
(declare-fun f_ackermann!0 () (_ BitVec 64))
(assert
 (not (fp.isNaN ((_ to_fp 11 53) f_ackermann!0))))
(assert
 (let ((?x8 ((_ to_fp 11 53) f_ackermann!0)))
(let ((?x18 (fp.sqrt roundNearestTiesToEven (fp.mul roundNearestTiesToEven ?x8 ?x8))))
(let ((?x24 (fp.mul roundNearestTiesToEven ?x18 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))))
(let ((?x11 (fp.abs ?x8)))
(let (($x20 (or (fp.isNaN (fp.mul roundNearestTiesToEven ?x11 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))) (fp.isNaN ?x18))))
(let (($x22 (or $x20 (fp.gt (fp.mul roundNearestTiesToEven ?x11 ((_ to_fp 11 53) (_ bv4607092346807469998 64))) ?x18))))
(not (or $x22 (or (or (fp.isNaN ?x11) (fp.isNaN ?x24)) (fp.lt ?x11 ?x24)))))))))))
(check-sat)
;   OK -- Elapsed: 1.679514e+03
;   Solvable: true
;     f = [0,0,0,0,0,0,240,127]

; Query 2 -- Type: InitialValues, Instructions: 5579
; Emited by klee::Z3SolverImpl::getConstraintLog()
(set-info :status unknown)
(declare-fun f_ackermann!0 () (_ BitVec 64))
(assert
 (not (fp.isNaN ((_ to_fp 11 53) f_ackermann!0))))
(assert
 (let ((?x8 ((_ to_fp 11 53) f_ackermann!0)))
 (let ((?x11 (fp.abs ?x8)))
 (let ((?x15 (fp.mul roundNearestTiesToEven ?x11 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))))
 (not (fp.isNaN ?x15))))))
(assert
 (let ((?x8 ((_ to_fp 11 53) f_ackermann!0)))
 (let ((?x19 (fp.sqrt roundNearestTiesToEven (fp.mul roundNearestTiesToEven ?x8 ?x8))))
 (not (fp.isNaN ?x19)))))
(assert
 (let ((?x8 ((_ to_fp 11 53) f_ackermann!0)))
 (let ((?x19 (fp.sqrt roundNearestTiesToEven (fp.mul roundNearestTiesToEven ?x8 ?x8))))
 (let ((?x11 (fp.abs ?x8)))
 (let ((?x15 (fp.mul roundNearestTiesToEven ?x11 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))))
 (not (fp.gt ?x15 ?x19)))))))
(assert
 (not (fp.isNaN (fp.abs ((_ to_fp 11 53) f_ackermann!0)))))
(assert
 (let ((?x8 ((_ to_fp 11 53) f_ackermann!0)))
 (let ((?x19 (fp.sqrt roundNearestTiesToEven (fp.mul roundNearestTiesToEven ?x8 ?x8))))
 (let ((?x26 (fp.mul roundNearestTiesToEven ?x19 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))))
 (not (fp.isNaN ?x26))))))
(assert
 (let ((?x8 ((_ to_fp 11 53) f_ackermann!0)))
 (let ((?x19 (fp.sqrt roundNearestTiesToEven (fp.mul roundNearestTiesToEven ?x8 ?x8))))
 (let ((?x26 (fp.mul roundNearestTiesToEven ?x19 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))))
 (let ((?x11 (fp.abs ?x8)))
 (not (fp.lt ?x11 ?x26)))))))
(assert
 (not false))
(check-sat)
;   OK -- Elapsed: 1.441376e+03
;   Solvable: true
;     f = [139,95,141,161,98,12,247,63]

; Query 3 -- Type: InitialValues, Instructions: 5579
; Emited by klee::Z3SolverImpl::getConstraintLog()
(set-info :status unknown)
(declare-fun f_ackermann!0 () (_ BitVec 64))
(assert
 (not (fp.isNaN ((_ to_fp 11 53) f_ackermann!0))))
(assert
 (let ((?x8 ((_ to_fp 11 53) f_ackermann!0)))
 (let ((?x11 (fp.abs ?x8)))
 (let ((?x15 (fp.mul roundNearestTiesToEven ?x11 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))))
 (not (fp.isNaN ?x15))))))
(assert
 (let ((?x8 ((_ to_fp 11 53) f_ackermann!0)))
 (let ((?x19 (fp.sqrt roundNearestTiesToEven (fp.mul roundNearestTiesToEven ?x8 ?x8))))
 (not (fp.isNaN ?x19)))))
(assert
 (let ((?x8 ((_ to_fp 11 53) f_ackermann!0)))
 (let ((?x19 (fp.sqrt roundNearestTiesToEven (fp.mul roundNearestTiesToEven ?x8 ?x8))))
 (let ((?x11 (fp.abs ?x8)))
 (let ((?x15 (fp.mul roundNearestTiesToEven ?x11 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))))
 (not (fp.gt ?x15 ?x19)))))))
(assert
 (not (fp.isNaN (fp.abs ((_ to_fp 11 53) f_ackermann!0)))))
(assert
 (let ((?x8 ((_ to_fp 11 53) f_ackermann!0)))
 (let ((?x19 (fp.sqrt roundNearestTiesToEven (fp.mul roundNearestTiesToEven ?x8 ?x8))))
 (let ((?x26 (fp.mul roundNearestTiesToEven ?x19 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))))
 (not (fp.isNaN ?x26))))))
(assert
 (let ((?x8 ((_ to_fp 11 53) f_ackermann!0)))
 (let ((?x19 (fp.sqrt roundNearestTiesToEven (fp.mul roundNearestTiesToEven ?x8 ?x8))))
 (let ((?x26 (fp.mul roundNearestTiesToEven ?x19 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))))
 (let ((?x11 (fp.abs ?x8)))
 (not (fp.lt ?x11 ?x26)))))))
(assert
 (let ((?x8 ((_ to_fp 11 53) f_ackermann!0)))
(let ((?x19 (fp.sqrt roundNearestTiesToEven (fp.mul roundNearestTiesToEven ?x8 ?x8))))
(let ((?x11 (fp.abs ?x8)))
(not (fp.eq ?x11 ?x19))))))
(check-sat)
;   FAIL -- Elapsed: 3.720509e+03
;   Failure reason: SOLVER TIMEOUT