test/regress/regress0/bug576a.smt2

   1 (set-logic QF_UF)
   2 (set-info :status sat)
   3 (declare-sort var 0)
   4 (declare-sort reg 0)
   5 (declare-fun a1_1 () var)
   6 (declare-fun a2_1 () var)
   7 (declare-fun c_3 () var)
   8 (declare-fun c_4 () var)
   9 (declare-fun b_3 () var)
  10 (declare-fun r0 () reg)
  11 (declare-fun r1 () reg)
  12 (declare-fun r2 () reg)
  13 (declare-fun r3 () reg)
  14 (declare-fun r4 () reg)
  15 (declare-fun r6 () reg)
  16 (assert (not (= r0 r1)))
  17 (assert (not (= r0 r2)))
  18 (assert (not (= r0 r3)))
  19 (assert (not (= r0 r4)))
  20 (assert (not (= r0 r6)))
  21 (assert (not (= r1 r2)))
  22 (assert (not (= r1 r3)))
  23 (assert (not (= r1 r4)))
  24 (assert (not (= r1 r6)))
  25 (assert (not (= r2 r3)))
  26 (assert (not (= r2 r4)))
  27 (assert (not (= r2 r6)))
  28 (assert (not (= r3 r4)))
  29 (assert (not (= r3 r6)))
  30 (assert (not (= r4 r6)))
  31 (declare-fun assign (var) reg)
  32 (assert (or (= (assign a1_1) r0) (= (assign a1_1) r1) (= (assign a1_1) r2) (= (assign a1_1) r3) (= (assign a1_1) r4) (= (assign a1_1) r6) ))
  33 (assert (or (= (assign a2_1) r0) (= (assign a2_1) r1) (= (assign a2_1) r2) (= (assign a2_1) r3) (= (assign a2_1) r4) (= (assign a2_1) r6) ))
  34 (assert (or (= (assign c_3) r0) (= (assign c_3) r1) (= (assign c_3) r2) (= (assign c_3) r3) (= (assign c_3) r4) (= (assign c_3) r6) ))
  35 (assert (or (= (assign c_4) r0) (= (assign c_4) r1) (= (assign c_4) r2) (= (assign c_4) r3) (= (assign c_4) r4) (= (assign c_4) r6) ))
  36 (assert (or (= (assign b_3) r0) (= (assign b_3) r1) (= (assign b_3) r2) (= (assign b_3) r3) (= (assign b_3) r4) (= (assign b_3) r6) ))
  37 (assert (not (= (assign a1_1) (assign c_4))))
  38 (assert (not (= (assign a2_1) (assign c_3))))
  39 (assert (not (= (assign a2_1) (assign b_3))))
  40 (assert (not (= (assign c_3) (assign b_3))))
  41 (assert (not (= (assign c_4) (assign b_3))))
  42 (assert (= (assign a1_1) r0))
  43 (assert (= (assign a2_1) r2))
  44 (assert (= (assign c_3) r1))
  45 (assert (= (assign c_4) r1))
  46 (assert (= (assign b_3) r0))
  47 (check-sat)
  48 (exit)