sign32.smt example fails with 'already declared' variable

[BwRy]

I was just following the SMT example (https://github.com/wmkhoo/taintgrind/wiki/Generating-SMT-Libv2-output) linked to on your README. Z3 gives the following output and error without specifying the second possible solution's BITVEC/bytes (e.g. hex 0, hex -1) for the integer variable a in the sign32.c test:

sat
(model 
  (define-fun a1ffefffc40 () (_ BitVec 8)
    #x00)
  (define-fun byte2 () (_ BitVec 8)
    #x00)
  (define-fun a1ffefffc41 () (_ BitVec 8)
    #x00)
  (define-fun a1ffefffc1e () (_ BitVec 8)
    #x00)
  (define-fun r16_903 () (_ BitVec 64)
    #x0000000000000000)
  (define-fun t52_1525 () (_ BitVec 64)
    #x0000000000000001)
  (define-fun byte3 () (_ BitVec 8)
    #x00)
  (define-fun t23_5467 () (_ BitVec 64)
    #x0000000000000000)
  (define-fun t40_2175 () (_ BitVec 1)
    #b1)
  (define-fun byte1 () (_ BitVec 8)
    #x00)
  (define-fun t49_2145 () (_ BitVec 64)
    #x0000000000000000)
  (define-fun t50_1483 () (_ BitVec 32)
    #x00000000)
  (define-fun a1ffefffc1c () (_ BitVec 8)
    #x00)
  (define-fun t45_2456 () (_ BitVec 64)
    #x0000000000000001)
  (define-fun r152_0 () (_ BitVec 64)
    #x0000000000000000)
  (define-fun t55_1487 () (_ BitVec 32)
    #x00000000)
  (define-fun t56_1209 () (_ BitVec 1)
    #b1)
  (define-fun a1ffefffc42 () (_ BitVec 8)
    #x00)
  (define-fun a1ffefffc1f () (_ BitVec 8)
    #x00)
  (define-fun t21_4678 () (_ BitVec 64)
    #x0000000000000000)
  (define-fun t24_4075 () (_ BitVec 32)
    #x00000000)
  (define-fun t53_1374 () (_ BitVec 1)
    #b1)
  (define-fun a1ffefffc43 () (_ BitVec 8)
    #x00)
  (define-fun r72_2 () (_ BitVec 64)
    #x0000000000000000)
  (define-fun byte0 () (_ BitVec 8)
    #x00)
  (define-fun t48_1543 () (_ BitVec 32)
    #x00000000)
  (define-fun t38_2103 () (_ BitVec 64)
    #x0000000000000000)
  (define-fun t47_1326 () (_ BitVec 64)
    #x0000000000000000)
  (define-fun t22_5669 () (_ BitVec 32)
    #x00000000)
  (define-fun t10_8245 () (_ BitVec 32)
    #x00000000)
  (define-fun a1ffefffc1d () (_ BitVec 8)
    #x00)
  (define-fun t51_1172 () (_ BitVec 64)
    #x0000000000000000)
  (define-fun t34_2061 () (_ BitVec 32)
    #x00000000)
)
(error "line 103 column 37: invalid declaration, constant 'r152_0' (with the given signature) already declared")
unsat
(error "line 127 column 10: model is not available")