Missing suffix in var when printing solution with --save

[nilehmann]

The following constraint

(qualif EqZero ((a0 int)) (a0 = 0))
(qualif GtZero ((a0 int)) (a0 > 0))
(qualif GeZero ((a0 int)) (a0 >= 0))
(qualif LtZero ((a0 int)) (a0 < 0))
(qualif LeZero ((a0 int)) (a0 <= 0))
(qualif Eq ((a0 int) (a1 int)) (a0 = a1))
(qualif Gt ((a0 int) (a1 int)) (a0 > a1))
(qualif Ge ((a0 int) (a1 int)) (a0 >= a1))
(qualif Lt ((a0 int) (a1 int)) (a0 < a1))
(qualif Le ((a0 int) (a1 int)) (a0 <= a1))
(qualif Le1 ((a0 int) (a1 int)) (a0 <= (a1 - 1)))
(data Pair 2 = [| Pair { fst: @(0), snd: @(1) } ])
(data Unit 0 = [| Unit { }])
(var $k0 ((int) (int)))

(constraint
  (forall ((a0 int) (true))
    (forall ((_ Unit) (a0 >= 0))
      (and
        (forall ((a1 int) (a1 = 0))
          (tag ($k0 a1 a0) "0")
        )
        (forall ((a2 int) (true))
          (forall ((_ Unit) ($k0 a2 a0))
            (and
              (forall ((_ Unit) (~(a2 < a0)))
                (tag (a2 = a0) "1")
              )
              (forall ((_ Unit) (a2 < a0))
                (forall ((a3 int) (a3 = (a2 + 1)))
                  (tag ($k0 a3 a0) "2")
                )
              )
            )
          )
        )
      )
    )
  )
)

produces the following output when I run fixpoint --save on it

Solution:
$k0 := nnf_arg##k0 >= 0
       && nnf_arg##k0 <= nnf_arg##k0

Non-cut kvars:

Seems like the pretty printing is missing the suffix indicating the variable.

[ranjitjhala]

with the above fix you get

Solution:
$k0 := $k0##0 >= 0
       && $k0##0 <= $k0##1