File: fuzz01.smtv1.smt2

package info (click to toggle)
cvc4 1.8-2
  • links: PTS, VCS
  • area: main
  • in suites: bullseye
  • size: 69,876 kB
  • sloc: cpp: 274,686; sh: 5,833; python: 1,893; java: 929; lisp: 763; ansic: 275; perl: 214; makefile: 22; awk: 2
file content (15 lines) | stat: -rw-r--r-- 13,894 bytes parent folder | download | duplicates (5) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
 
(set-option :incremental false)
(set-info :status sat)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 15))
(declare-fun v1 () (_ BitVec 3))
(declare-fun v2 () (_ BitVec 11))
(declare-fun a3 () (Array (_ BitVec 3) (_ BitVec 5)))
(declare-fun a4 () (Array (_ BitVec 5) (_ BitVec 15)))
(declare-fun a5 () (Array (_ BitVec 2) (_ BitVec 13)))
(declare-fun a6 () (Array (_ BitVec 1) (_ BitVec 13)))
(declare-fun a7 () (Array (_ BitVec 3) (_ BitVec 7)))
(declare-fun a8 () (Array (_ BitVec 4) (_ BitVec 14)))
(declare-fun a9 () (Array (_ BitVec 8) (_ BitVec 5)))
(declare-fun a10 () (Array (_ BitVec 3) (_ BitVec 14)))
(check-sat-assuming ( (let ((_let_0 (bvlshr ((_ zero_extend 7) (_ bv13 4)) v2))) (let ((_let_1 (ite (= (_ bv1 1) ((_ extract 4 4) (_ bv33 9))) (_ bv19308 16) ((_ sign_extend 9) (_ bv18 7))))) (let ((_let_2 (ite (bvugt (_ bv33 9) ((_ zero_extend 8) (_ bv1 1))) (_ bv1 1) (_ bv0 1)))) (let ((_let_3 (bvnor ((_ zero_extend 8) v1) v2))) (let ((_let_4 (bvnot _let_3))) (let ((_let_5 (ite (bvsge ((_ sign_extend 5) (_ bv33 6)) v2) (_ bv1 1) (_ bv0 1)))) (let ((_let_6 (ite (bvsge (_ bv1572 12) ((_ zero_extend 1) _let_4)) (_ bv1 1) (_ bv0 1)))) (let ((_let_7 (ite (bvsle v0 ((_ sign_extend 4) v2)) (_ bv1 1) (_ bv0 1)))) (let ((_let_8 (select (store a6 ((_ extract 2 2) v1) ((_ zero_extend 12) _let_6)) (_ bv1 1)))) (let ((_let_9 (select (store a10 ((_ extract 7 5) _let_4) ((_ zero_extend 10) (_ bv13 4))) ((_ zero_extend 2) _let_2)))) (let ((_let_10 (select a5 ((_ sign_extend 1) _let_2)))) (let ((_let_11 (select a4 ((_ sign_extend 4) _let_6)))) (let ((_let_12 (store a7 ((_ extract 7 5) (_ bv19308 16)) ((_ zero_extend 6) (_ bv1 1))))) (let ((_let_13 (select a4 ((_ extract 5 1) (_ bv33 6))))) (let ((_let_14 (select (store a6 (_ bv1 1) ((_ zero_extend 8) (select (store a9 ((_ extract 7 0) _let_4) ((_ extract 8 4) v0)) ((_ extract 13 6) (_ bv19308 16))))) ((_ extract 0 0) _let_4)))) (let ((_let_15 (select _let_12 ((_ extract 2 0) (_ bv18 7))))) (let ((_let_16 (bvxor ((_ zero_extend 8) (select a3 ((_ zero_extend 2) _let_5))) _let_14))) (let ((_let_17 (bvneg (select _let_12 ((_ extract 5 3) v2))))) (let ((_let_18 (ite (bvsge ((_ zero_extend 4) _let_3) _let_13) (_ bv1 1) (_ bv0 1)))) (let ((_let_19 (bvor _let_8 ((_ zero_extend 12) (ite (bvuge (_ bv33 9) ((_ zero_extend 2) _let_17)) (_ bv1 1) (_ bv0 1)))))) (let ((_let_20 (bvnot (_ bv33 6)))) (let ((_let_21 (ite (bvsge _let_9 ((_ sign_extend 1) _let_14)) (_ bv1 1) (_ bv0 1)))) (let ((_let_22 (bvxor _let_15 _let_15))) (let ((_let_23 ((_ sign_extend 2) _let_0))) (let ((_let_24 (bvand _let_7 (ite (bvuge (_ bv33 9) ((_ zero_extend 2) _let_17)) (_ bv1 1) (_ bv0 1))))) (let ((_let_25 ((_ extract 8 2) _let_4))) (let ((_let_26 ((_ rotate_right 0) (_ bv1 1)))) (let ((_let_27 ((_ zero_extend 7) _let_22))) (let ((_let_28 ((_ rotate_right 4) ((_ repeat 10) _let_5)))) (let ((_let_29 ((_ sign_extend 8) _let_17))) (let ((_let_30 (bvshl v0 _let_29))) (let ((_let_31 (bvshl (select (store a9 ((_ extract 7 0) _let_4) ((_ extract 8 4) v0)) ((_ extract 13 6) (_ bv19308 16))) ((_ sign_extend 4) (ite (= a8 a8) (_ bv1 1) (_ bv0 1)))))) (let ((_let_32 (bvxor _let_1 ((_ sign_extend 15) _let_18)))) (let ((_let_33 (bvnor ((_ sign_extend 13) (ite (= a8 a8) (_ bv1 1) (_ bv0 1))) _let_27))) (let ((_let_34 ((_ extract 0 0) _let_6))) (let ((_let_35 (bvand ((_ sign_extend 1) _let_11) (_ bv19308 16)))) (let ((_let_36 (bvashr (select a4 ((_ extract 6 2) _let_4)) (bvadd ((_ zero_extend 2) _let_10) _let_13)))) (let ((_let_37 ((_ repeat 1) (_ bv19308 16)))) (let ((_let_38 (ite (bvule ((_ sign_extend 8) (_ bv18 7)) v0) (_ bv1 1) (_ bv0 1)))) (let ((_let_39 (ite (= ((_ sign_extend 6) (select (store a9 ((_ extract 9 2) _let_3) ((_ extract 5 1) _let_0)) ((_ zero_extend 7) (ite (= a8 a8) (_ bv1 1) (_ bv0 1))))) _let_0) (_ bv1 1) (_ bv0 1)))) (let ((_let_40 ((_ repeat 1) ((_ repeat 10) _let_5)))) (let ((_let_41 (bvashr ((_ sign_extend 2) _let_19) (bvadd ((_ zero_extend 2) _let_10) _let_13)))) (let ((_let_42 ((_ rotate_left 1) ((_ repeat 10) _let_5)))) (let ((_let_43 (bvor _let_4 ((_ sign_extend 8) ((_ rotate_right 2) v1))))) (let ((_let_44 ((_ extract 12 10) _let_37))) (let ((_let_45 ((_ zero_extend 14) (ite (bvsgt ((_ zero_extend 8) _let_20) (bvlshr ((_ zero_extend 11) v1) _let_9)) (_ bv1 1) (_ bv0 1))))) (let ((_let_46 (ite (bvslt _let_45 (bvadd ((_ zero_extend 2) _let_10) _let_13)) (_ bv1 1) (_ bv0 1)))) (let ((_let_47 ((_ sign_extend 8) v1))) (let ((_let_48 ((_ zero_extend 4) _let_43))) (let ((_let_49 ((_ sign_extend 5) _let_42))) (let ((_let_50 (bvsge ((_ sign_extend 2) _let_43) _let_14))) (let ((_let_51 ((_ zero_extend 10) _let_20))) (let ((_let_52 ((_ zero_extend 10) (ite (= a8 a8) (_ bv1 1) (_ bv0 1))))) (let ((_let_53 (or (not (bvult (concat (ite (bvsgt ((_ zero_extend 8) _let_20) (bvlshr ((_ zero_extend 11) v1) _let_9)) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_4 ((_ sign_extend 10) _let_2)) (_ bv1 1) (_ bv0 1))) (concat (ite (bvsgt ((_ zero_extend 8) _let_20) (bvlshr ((_ zero_extend 11) v1) _let_9)) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_4 ((_ sign_extend 10) _let_2)) (_ bv1 1) (_ bv0 1))))) (bvule v2 ((_ zero_extend 6) (select (store a9 ((_ extract 9 2) _let_3) ((_ extract 5 1) _let_0)) ((_ zero_extend 7) (ite (= a8 a8) (_ bv1 1) (_ bv0 1))))))))) (let ((_let_54 (not (bvsge ((_ zero_extend 2) _let_5) v1)))) (let ((_let_55 (=> (and (bvult ((_ sign_extend 5) _let_0) (bvneg _let_1)) (xor (bvsgt (bvlshr ((_ zero_extend 11) v1) _let_9) ((_ zero_extend 8) _let_20)) (bvult _let_2 _let_39))) (bvsge ((_ sign_extend 3) _let_10) (bvadd ((_ zero_extend 5) v2) (_ bv19308 16)))))) (let ((_let_56 (and (= (bvsle (bvadd ((_ zero_extend 2) _let_10) _let_13) _let_45) (bvugt _let_10 ((_ zero_extend 12) (ite (bvsgt ((_ sign_extend 9) (_ bv13 4)) _let_23) (_ bv1 1) (_ bv0 1))))) (bvuge ((_ sign_extend 13) _let_18) (bvlshr ((_ zero_extend 11) v1) _let_9))))) (let ((_let_57 (=> (=> (=> (ite (xor (bvugt ((_ zero_extend 6) (_ bv18 7)) _let_10) (=> (bvult ((_ zero_extend 13) ((_ rotate_right 0) _let_5)) _let_9) (bvsgt (bvneg _let_1) ((_ zero_extend 15) _let_24)))) (bvugt _let_4 ((_ zero_extend 10) _let_2)) (=> (or (xor (xor (bvslt ((_ zero_extend 9) (select a3 ((_ zero_extend 2) _let_5))) (bvlshr ((_ zero_extend 11) v1) _let_9)) (bvugt _let_43 _let_47)) (bvsge _let_15 ((_ zero_extend 6) _let_18))) (bvslt ((_ zero_extend 4) _let_17) _let_43)) (and (bvsge ((_ sign_extend 2) (ite (= a8 a8) (_ bv1 1) (_ bv0 1))) ((_ rotate_right 2) v1)) (bvsgt (bvadd ((_ zero_extend 2) _let_10) _let_13) ((_ sign_extend 14) (ite (= a8 a8) (_ bv1 1) (_ bv0 1))))))) (ite (xor (bvugt ((_ zero_extend 6) (_ bv18 7)) _let_10) (=> (bvult ((_ zero_extend 13) ((_ rotate_right 0) _let_5)) _let_9) (bvsgt (bvneg _let_1) ((_ zero_extend 15) _let_24)))) (bvugt _let_4 ((_ zero_extend 10) _let_2)) (=> (or (xor (xor (bvslt ((_ zero_extend 9) (select a3 ((_ zero_extend 2) _let_5))) (bvlshr ((_ zero_extend 11) v1) _let_9)) (bvugt _let_43 _let_47)) (bvsge _let_15 ((_ zero_extend 6) _let_18))) (bvslt ((_ zero_extend 4) _let_17) _let_43)) (and (bvsge ((_ sign_extend 2) (ite (= a8 a8) (_ bv1 1) (_ bv0 1))) ((_ rotate_right 2) v1)) (bvsgt (bvadd ((_ zero_extend 2) _let_10) _let_13) ((_ sign_extend 14) (ite (= a8 a8) (_ bv1 1) (_ bv0 1)))))))) (= (bvsge ((_ sign_extend 11) ((_ extract 7 6) (_ bv1572 12))) _let_14) (bvugt (ite (bvuge (_ bv33 9) ((_ zero_extend 2) _let_17)) (_ bv1 1) (_ bv0 1)) _let_21))) (bvsle ((_ zero_extend 3) _let_10) _let_37)))) (xor (and (and (xor _let_55 _let_55) (not (bvsle ((_ sign_extend 7) ((_ extract 7 6) (_ bv1572 12))) (_ bv33 9)))) (ite (ite (=> (= (xor (and (or (or (bvsgt _let_10 ((_ sign_extend 12) (ite (= a8 a8) (_ bv1 1) (_ bv0 1)))) (bvsle ((_ zero_extend 2) _let_46) _let_44)) (and (bvult ((_ zero_extend 14) _let_46) (select a4 ((_ extract 6 2) _let_4))) (xor (bvsgt _let_1 ((_ zero_extend 15) _let_7)) (bvult ((_ sign_extend 1) _let_41) _let_1)))) (bvugt ((_ zero_extend 10) _let_26) _let_43)) (not (and (= (xor (bvuge _let_28 ((_ zero_extend 9) _let_2)) (bvsgt _let_49 _let_41)) (bvslt ((_ zero_extend 1) _let_23) (bvlshr ((_ zero_extend 11) v1) _let_9))) (bvsge _let_33 ((_ sign_extend 13) (ite (bvsle _let_4 ((_ sign_extend 10) _let_2)) (_ bv1 1) (_ bv0 1))))))) (xor (=> (xor (ite (bvule _let_37 ((_ zero_extend 10) (_ bv33 6))) (not (=> (bvugt _let_25 ((_ sign_extend 6) _let_6)) (bvult _let_48 _let_30))) (xor (bvsle _let_0 ((_ sign_extend 10) (ite (= a8 a8) (_ bv1 1) (_ bv0 1)))) (bvsge (_ bv18 7) _let_17))) (bvsgt _let_10 ((_ sign_extend 12) _let_26))) (bvule ((_ zero_extend 11) (select a3 ((_ zero_extend 2) _let_5))) _let_32)) (and (and (bvult ((_ sign_extend 12) _let_46) (bvmul _let_8 ((_ sign_extend 2) _let_4))) (or (bvult ((_ zero_extend 3) _let_44) (_ bv33 6)) (ite (bvsle _let_46 (ite (bvuge (_ bv33 9) ((_ zero_extend 2) _let_17)) (_ bv1 1) (_ bv0 1))) (bvugt (bvlshr ((_ zero_extend 11) v1) _let_9) ((_ zero_extend 13) (ite (bvsle _let_4 ((_ sign_extend 10) _let_2)) (_ bv1 1) (_ bv0 1)))) (bvsge ((_ zero_extend 9) (select a3 ((_ zero_extend 2) _let_5))) _let_27)))) (not (bvsle _let_52 _let_3))))) (ite _let_56 _let_56 (= _let_54 _let_54))) (= (xor (or (bvsle _let_41 _let_36) (= (bvugt _let_35 ((_ sign_extend 11) (ite (= (_ bv1 1) ((_ extract 6 6) _let_30)) ((_ zero_extend 4) _let_5) (select a3 ((_ zero_extend 2) _let_5))))) (=> (bvule (bvneg _let_1) ((_ sign_extend 6) _let_40)) (xor (ite (distinct _let_8 ((_ sign_extend 4) (_ bv33 9))) (=> (bvult _let_17 ((_ sign_extend 2) (select (store a9 ((_ extract 7 0) _let_4) ((_ extract 8 4) v0)) ((_ extract 13 6) (_ bv19308 16))))) (and (= _let_19 _let_19) (distinct _let_17 _let_17))) (bvslt (bvlshr ((_ zero_extend 11) v1) _let_9) ((_ zero_extend 7) (_ bv18 7)))) (bvugt ((_ zero_extend 9) _let_7) _let_28))))) (xor (and (bvugt ((_ zero_extend 3) _let_25) _let_40) (and (bvsge _let_52 _let_4) (bvule _let_30 ((_ zero_extend 8) (select _let_12 ((_ extract 5 3) v2)))))) (and (ite (and (= ((_ sign_extend 7) _let_17) _let_9) (bvugt ((_ sign_extend 11) ((_ extract 7 6) (_ bv1572 12))) _let_16)) (bvslt _let_48 _let_41) (or (= (bvsle _let_22 ((_ zero_extend 6) _let_18)) (bvult ((_ zero_extend 10) _let_31) _let_11)) (xor (bvule _let_15 ((_ zero_extend 5) ((_ extract 7 6) (_ bv1572 12)))) (= _let_23 _let_19)))) (bvule _let_51 (bvneg _let_1))))) (and (not (xor (bvule ((_ zero_extend 4) (ite (= a8 a8) (_ bv1 1) (_ bv0 1))) (select (store a9 ((_ extract 9 2) _let_3) ((_ extract 5 1) _let_0)) ((_ zero_extend 7) (ite (= a8 a8) (_ bv1 1) (_ bv0 1))))) (bvslt _let_11 v0))) (not (xor (bvuge ((_ zero_extend 9) (ite (bvsle _let_4 ((_ sign_extend 10) _let_2)) (_ bv1 1) (_ bv0 1))) _let_40) (bvult ((_ sign_extend 14) _let_46) _let_11))))) (= (or (= ((_ sign_extend 9) _let_7) _let_28) (bvslt ((_ sign_extend 12) _let_44) _let_13)) (not (and (= _let_57 _let_57) (bvslt _let_27 ((_ sign_extend 8) (_ bv33 6))))))) (not (ite (=> (and (bvslt ((_ zero_extend 10) _let_7) v2) (or (ite (bvuge ((_ sign_extend 2) (_ bv1572 12)) _let_33) (bvsge ((_ sign_extend 13) _let_5) (bvlshr ((_ zero_extend 11) v1) _let_9)) (bvuge _let_31 ((_ zero_extend 4) (ite (bvslt ((_ zero_extend 10) v1) _let_19) (_ bv1 1) (_ bv0 1))))) (not (or (= _let_28 ((_ zero_extend 9) _let_39)) (bvslt (bvlshr ((_ zero_extend 11) v1) _let_9) ((_ sign_extend 7) (select _let_12 ((_ extract 5 3) v2)))))))) (= (=> (= (bvsle ((_ zero_extend 1) (_ bv33 6)) (select _let_12 ((_ extract 5 3) v2))) (bvsgt _let_14 _let_16)) (= ((_ zero_extend 5) (_ bv33 9)) _let_33)) (ite (bvsgt ((_ zero_extend 13) _let_44) _let_32) (distinct _let_36 ((_ sign_extend 3) (_ bv1572 12))) (ite (bvugt ((_ sign_extend 14) _let_24) (bvadd ((_ zero_extend 2) _let_10) _let_13)) (distinct ((_ sign_extend 13) (_ bv1 1)) (bvlshr ((_ zero_extend 11) v1) _let_9)) (= _let_36 ((_ zero_extend 8) (_ bv18 7))))))) (xor (bvult _let_42 ((_ repeat 10) _let_5)) (= (ite (or (xor (bvuge _let_9 ((_ zero_extend 13) _let_18)) (and (bvule ((_ zero_extend 4) _let_0) _let_13) (bvult _let_16 ((_ zero_extend 9) (_ bv13 4))))) (or (and (xor (bvuge _let_41 ((_ sign_extend 2) _let_8)) (bvslt ((_ sign_extend 4) (ite (bvsle _let_4 ((_ sign_extend 10) _let_2)) (_ bv1 1) (_ bv0 1))) (select (store a9 ((_ extract 9 2) _let_3) ((_ extract 5 1) _let_0)) ((_ zero_extend 7) (ite (= a8 a8) (_ bv1 1) (_ bv0 1)))))) (not (bvugt ((_ zero_extend 14) _let_18) _let_13))) (xor (or (bvule _let_17 ((_ zero_extend 6) _let_5)) (bvult _let_49 _let_30)) (bvsge _let_14 ((_ sign_extend 3) _let_28))))) (bvuge ((_ zero_extend 9) (_ bv1 1)) _let_40) (=> (= ((_ zero_extend 5) _let_0) _let_35) (not (bvsge _let_16 ((_ zero_extend 12) _let_34))))) (not (= _let_5 _let_7)))) (=> (or (=> (not (= v0 _let_29)) (bvsge _let_20 ((_ zero_extend 5) _let_34))) (bvsgt _let_35 ((_ zero_extend 2) _let_9))) (=> (distinct ((_ sign_extend 7) (_ bv18 7)) _let_27) (distinct _let_36 _let_36))))) (=> (bvule _let_11 ((_ sign_extend 12) v1)) (bvuge ((_ sign_extend 6) (ite (bvsle _let_4 ((_ sign_extend 10) _let_2)) (_ bv1 1) (_ bv0 1))) _let_15)))) (= (=> _let_50 _let_50) (= (bvsge _let_37 _let_51) (or (xor (bvuge _let_17 ((_ sign_extend 2) (select (store a9 ((_ extract 9 2) _let_3) ((_ extract 5 1) _let_0)) ((_ zero_extend 7) (ite (= a8 a8) (_ bv1 1) (_ bv0 1)))))) (= (not (= _let_30 ((_ zero_extend 2) _let_14))) (ite (= (bvule _let_33 ((_ zero_extend 13) _let_7)) (distinct (_ bv19308 16) _let_37)) (bvsge _let_27 ((_ sign_extend 7) _let_22)) (bvsle _let_28 ((_ zero_extend 1) (_ bv33 9)))))) (=> (ite _let_53 (not (=> (xor (bvule _let_16 _let_10) (bvule _let_43 ((_ sign_extend 4) _let_17))) (bvslt _let_28 ((_ sign_extend 9) (ite (bvsle _let_4 ((_ sign_extend 10) _let_2)) (_ bv1 1) (_ bv0 1)))))) _let_53) (xor (ite (= (bvugt _let_47 v2) (distinct _let_15 ((_ zero_extend 1) _let_20))) (xor (= a3 a3) (distinct _let_21 _let_38)) (= (bvugt ((_ zero_extend 11) _let_18) (_ bv1572 12)) (bvslt v2 _let_0))) (not (not (distinct ((_ sign_extend 12) _let_38) _let_19))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))