1 2 3 4 5 6 7 8
; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) (declare-fun t () Int) (assert (> t 0)) (assert (not (= t (bv2nat ((_ int2bv 16) t))))) (check-sat)