1 2 3 4 5
(set-option :incremental false) (set-info :status unsat) (set-logic QF_BV) (declare-fun x () (_ BitVec 32)) (check-sat-assuming ( (not (= ((_ extract 4 4) ((_ extract 31 0) x)) ((_ extract 4 4) x))) ))