blob: a48156e2727219f4f016098c7379ea904fc89385 (
plain)
1
2
3
4
5
6
7
8
9
|
(set-option :incremental false)
(set-info :status unsat)
(set-logic QF_AUFBV)
(declare-fun a1179 () (Array (_ BitVec 6) (_ BitVec 32)))
(declare-fun reset_3 () (_ BitVec 1))
(declare-fun full_fq_3 () (_ BitVec 1))
(declare-fun a741 () (Array (_ BitVec 6) (_ BitVec 32)))
(declare-fun a960 () (Array (_ BitVec 6) (_ BitVec 32)))
(check-sat-assuming ( (not (= (_ bv0 1) (bvand (bvand (ite (= a1179 a960) (_ bv1 1) (_ bv0 1)) (bvand (ite (= a960 (ite (= (_ bv1 1) full_fq_3) a741 (store a741 (_ bv0 6) (_ bv0 32)))) (_ bv1 1) (_ bv0 1)) (bvand reset_3 (bvnot (bvand (bvnot (ite (= (_ bv0 1) full_fq_3) (_ bv1 1) (_ bv0 1))) reset_3))))) (ite (= (_ bv1 32) (select a1179 (_ bv0 6))) (_ bv1 1) (_ bv0 1))))) ))
|
