test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2

   1 ;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-models --no-produce-unsat-cores
   2 ;EXPECT: unsat
   3
   4 (set-logic QF_UFBV)
   5 (declare-fun z$n0s32 () (_ BitVec 32))
   6 (declare-fun dataOut () (_ BitVec 32))
   7 (declare-fun z$2 () (_ BitVec 1))
   8 (declare-fun stageOne () (_ BitVec 32))
   9 (declare-fun z$4 () (_ BitVec 1))
  10 (declare-fun stageTwo () (_ BitVec 32))
  11 (declare-fun z$6 () (_ BitVec 1))
  12 (declare-fun tmp_stageOne () (_ BitVec 32))
  13 (declare-fun z$8 () (_ BitVec 1))
  14 (declare-fun tmp_stageTwo () (_ BitVec 32))
  15 (declare-fun z$10 () (_ BitVec 1))
  16 (declare-fun reset_ () (_ BitVec 1))
  17 (declare-fun z$14 () (_ BitVec 1))
  18 (declare-fun Add_32_32_32 ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
  19 (declare-fun z$15 () (_ BitVec 32))
  20 (declare-fun z$17 () (_ BitVec 32))
  21 (declare-fun dataOut$next () (_ BitVec 32))
  22 (declare-fun z$19 () (_ BitVec 1))
  23 (declare-fun c1 () (_ BitVec 32))
  24 (declare-fun dataIn () (_ BitVec 32))
  25 (declare-fun z$23 () (_ BitVec 32))
  26 (declare-fun stageOne$next () (_ BitVec 32))
  27 (declare-fun z$25 () (_ BitVec 1))
  28 (declare-fun c2 () (_ BitVec 32))
  29 (declare-fun z$28 () (_ BitVec 32))
  30 (declare-fun stageTwo$next () (_ BitVec 32))
  31 (declare-fun z$30 () (_ BitVec 1))
  32 (declare-fun tmp_stageOne$next () (_ BitVec 32))
  33 (declare-fun z$32 () (_ BitVec 1))
  34 (declare-fun tmp_stageTwo$next () (_ BitVec 32))
  35 (declare-fun z$34 () (_ BitVec 1))
  36 (declare-fun z$35 () (_ BitVec 1))
  37 (declare-fun z$55 () (_ BitVec 32))
  38 (declare-fun z$57 () (_ BitVec 1))
  39 (declare-fun z$58 () (_ BitVec 1))
  40 (declare-fun z$59 () (_ BitVec 1))
  41 (declare-fun prop$next () (_ BitVec 1))
  42 (declare-fun z$61 () (_ BitVec 1))
  43 (declare-fun z$54 () (_ BitVec 1))
  44 (declare-fun z$63 () (_ BitVec 1))
  45 (assert
  46  (= z$15 (Add_32_32_32 stageTwo stageOne)))
  47 (assert
  48  (= z$17 (ite (= z$14 (_ bv1 1)) z$15 z$n0s32)))
  49 (assert
  50  (= z$19 (ite (= dataOut$next z$17) (_ bv1 1) (_ bv0 1))))
  51 (assert
  52  (= z$25 (ite (= stageOne$next z$23) (_ bv1 1) (_ bv0 1))))
  53
  54
  55 (assert
  56  (= z$32 (ite (= tmp_stageOne$next stageOne) (_ bv1 1) (_ bv0 1))))
  57 (assert
  58  (= z$34 (ite (= tmp_stageTwo$next stageTwo) (_ bv1 1) (_ bv0 1))))
  59 (assert
  60  (let (($x130 (and (= z$19 (_ bv1 1)) (= z$25 (_ bv1 1)) (= z$30 (_ bv1 1)) (= z$32 (_ bv1 1)) (= z$34 (_ bv1 1)))))
  61  (= z$35 (ite $x130 (_ bv1 1) (_ bv0 1)))))
  62 (assert
  63  (= z$55 (Add_32_32_32 tmp_stageTwo$next tmp_stageOne$next)))
  64 (assert
  65  (= z$57 (ite (= dataOut$next z$55) (_ bv1 1) (_ bv0 1))))
  66 (assert
  67  (= z$58 (ite (= dataOut$next z$n0s32) (_ bv1 1) (_ bv0 1))))
  68 (assert
  69  (= z$59 (ite (or (= z$57 (_ bv1 1)) (= z$58 (_ bv1 1))) (_ bv1 1) (_ bv0 1))))
  70 (assert
  71  (= z$61 (ite (= prop$next z$59) (_ bv1 1) (_ bv0 1))))
  72 (assert
  73  (= z$54 (ite (= prop$next (_ bv0 1)) (_ bv1 1) (_ bv0 1))))
  74 (assert
  75  (let (($x52 (= z$2 (_ bv1 1))))
  76  (let (($x165 (and $x52 (= z$4 (_ bv1 1)) (= z$6 (_ bv1 1)) (= z$8 (_ bv1 1)) (= z$10 (_ bv1 1)) (= z$35 (_ bv1 1)) (= z$61 (_ bv1 1)) (= z$54 (_ bv1 1)))))
  77  (= z$63 (ite $x165 (_ bv1 1) (_ bv0 1))))))
  78 (assert
  79  (= z$63 (_ bv1 1)))
  80 (check-sat)
  81 (exit)