[925] % timeout -s 9 8 z3 small.smt2 >& out.txt
Killed
[926] % tail -5 out.txt
ASSERTION VIOLATION
File: ../src/nlsat/nlsat_solver.cpp
Line: 562
a->ref_count() == 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
[927] % 
[927] % cat small.smt2
(set-option :nlsat.check_lemmas true)
(set-option :nlsat.shuffle_vars true)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun s () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun u () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun t () Real)
(declare-fun o () Real)
(declare-fun v () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(assert (not (forall ((f Real)) (= (<= h l 0.0) (<= 0.0 g)))))
(assert
 (exists ((r Real))
  (or
   (and
    (or
     (and
      (or
       (and
        (and (= o q) (= (+ (* (/ 4 c g)) j) (- b u) o (/ s i)))
        (< m (/ 7 a f) t))
       (<= 0.0 p))
      (> p (/ 4 b u)))))
   (>= m (* (* (+ (+ (* (- 4 c))))) (- g))))))
(assert (= c (+ g n)))
(assert (distinct d (/ h q)))
(assert (distinct e (/ j v k t)))
(check-sat)
[928] %