1 2 3 4 5 6
(set-option :incremental false) (set-info :status sat) (set-logic QF_AUFBV) (declare-fun a5 () (Array (_ BitVec 6) (_ BitVec 11))) (declare-fun v2 () (_ BitVec 1)) (check-sat-assuming ( (=> (= (_ bv0 11) (select a5 ((_ extract 7 2) ((_ sign_extend 9) v2)))) (bvule (select a5 (_ bv0 6)) (_ bv0 11))) ))