(set-logic QF_BV)
 (set-option :opt.priority pareto)
 (set-option :rewriter.cache_all true)
 (declare-fun v0 () Bool)
 (declare-fun v1 () Bool)
 (declare-fun v2 () Bool)
 (declare-fun bv_21-0 () (_ BitVec 21))
 (declare-fun bv_7-0 () (_ BitVec 7))
 (declare-fun bv_50-0 () (_ BitVec 50))
 (declare-fun bv_11-0 () (_ BitVec 11))
 (declare-fun v3 () Bool)
 (declare-fun v4 () Bool)
 (assert-soft v0 :weight 8)
 (push 4)
 (maximize bv_7-0)
 (minimize bv_11-0)
 (minimize bv_21-0)
 (minimize bv_50-0)
 (check-sat)
 (declare-fun v12 () Bool)
 (assert-soft (=> v0 v12) :weight 5)
 (declare-fun v13 () Bool)
 (push 1)
 (declare-fun v14 () Bool)
 (declare-fun v15 () Bool)
 (declare-fun v16 () Bool)
 (declare-fun v17 () Bool)
 (declare-fun v18 () Bool)
 (assert-soft (and v2 v2 (bvugt (bvnor #x46 #x46) #x1c) v1 v2 (and (distinct v4 v3 v0) v1 (distinct v4 v3 v0) v12)) :weight 7)
 (declare-fun v19 () Bool)
 (push 2)
 (assert-soft (distinct (bvnor bv_11-0 bv_11-0) (bvnor bv_11-0 bv_11-0) bv_11-0 (bvnor bv_11-0 bv_11-0)) :weight 18)
 (declare-fun v23 () Bool)
 (declare-fun v25 () Bool)
 (declare-fun v26 () Bool)
 (declare-fun v29 () Bool)
 (push 1)
 (push 3)
 (declare-fun v30 () Bool)
 (pop 1)
 (declare-fun v34 () Bool)
 (declare-fun v36 () Bool)
 (assert (= (bvadd #b10 #b10) #b10 (bvadd #b10 #b10) (bvadd #b10 #b10)))
 (push 4)
 (declare-fun v39 () Bool)
 (declare-fun v40 () Bool)
 (pop 9)
 (declare-fun v41 () Bool)
 (assert (not (=> v0 v12)))
 (declare-fun v42 () Bool)
 (assert (= v16 v19 v17))
 (declare-fun v44 () Bool)
 (assert-soft (not v3) :weight 5)
 (declare-fun v45 () Bool)
 (declare-fun bv_10-0 () (_ BitVec 10))
 (assert-soft v17 :weight 3)
 (declare-fun v46 () Bool)
 (assert-soft (or (distinct v13 (bvugt (bvnor #x46 #x46) #x1c) v13 v14 v2 (=> v2 v0) v16) (distinct v4 v3 v0) v12 v45 (= (bvadd #b10 #b10) #b10 (bvadd #b10 #b10) (bvadd #b10 #b10)) v1) :weight 16)
 (assert (not (and (distinct v4 v3 v0) v1 (distinct v4 v3 v0) v12)))
 (declare-fun v47 () Bool)
 (assert-soft v1 :weight 1)
 (minimize bv_7-0)
 (maximize bv_10-0)
 (maximize bv_11-0)
 (minimize bv_21-0)
 (minimize bv_50-0)
 (check-sat)
 (push 3)
 (declare-fun v48 () Bool)
 (pop 3)
 (pop 2)
 (declare-fun v60 () Bool)
 (declare-fun v61 () Bool)
 (declare-fun v62 () Bool)
 (declare-fun v63 () Bool)
 (assert-soft (and v60 v63 v61 (xor v4 v0 v3 v1)) :weight 20)
 (assert-soft (= v4 v2 (bvule bv_11-0 bv_11-0) (and v60 v63 v61 (xor v4 v0 v3 v1))) :weight 1)
 (push 3)
 (assert-soft v2 :weight 7)
 (declare-fun bv_7-2 () (_ BitVec 7))
 (assert-soft (xor v60 v2 (=> v2 v0)) :weight 16)
 (declare-fun v64 () Bool)
 (declare-fun bv_44-0 () (_ BitVec 44))
 (assert-soft (not (=> v2 v0)) :weight 14)
 (declare-fun v65 () Bool)
 (assert-soft (=> v64 (bvslt #b100000 #b100000)) :weight 1)
 (declare-fun v66 () Bool)
 (assert-soft (or v63 v66 (distinct bv_11-0 bv_11-0) v1 (and (bvslt #b100000 #b100000) (=> v64 (bvslt #b100000 #b100000)) v63)) :weight 20)
 (push 5)
 (minimize bv_7-0)
 (maximize bv_7-2)
 (maximize bv_11-0)
 (minimize bv_21-0)
 (minimize bv_44-0)
 (maximize bv_50-0)
 (minimize (bvadd bv_7-0 bv_7-2))
 (check-sat)