1 2 3 4 5
(set-logic HO_ALL) (set-info :status sat) (declare-fun p ((_ BitVec 17) (_ BitVec 16)) Bool) (assert (p (_ bv0 17) ((_ sign_extend 15) (ite (p (_ bv0 17) (_ bv0 16)) (_ bv1 1) (_ bv0 1))))) (check-sat)