Scrape fails to find qualifier

[nilehmann]

This is probably not a bug, but I found the behavior unintuitive when working on the source code that generated the constraint. Maybe we can improve the implementation of scrape to handle this case.

I have a code in Flux with an assert like this: assert(i < 10 && i >= 2). The code generates the following constraint that requires the qualifier x >= 2, but scrape=both fails to find it.

(fixpoint "--scrape=both")

// (qualif Gte2 ((a0 int)) (a0 >= 2))
(data Unit 0 = [| Unit { }])
(var $k0 ((int))) 
(var $k1 ((bool) (int)))
(var $k2 ((int) (int) (bool))) 

(constraint
  (and
    (forall ((a0 int) (a0 = 2))
      (tag ($k0 a0) "0")
    )
    (forall ((a1 int) (true))
      (forall ((_ Unit) ($k0 a1))
        (forall ((_ Unit) ((a1 < 10) = true))
          (forall ((_ Unit) (a1 >= 0))
            (and
              (forall ((_ Unit) (~(a1 < 10)))
                (forall ((a2 bool) (a2 = false))
                  (tag ($k1 a2 a1) "1")
                )
              )
              (forall ((_ Unit) (a1 < 10))
                (forall ((a3 bool) (a3 = (a1 >= 2)))
                  (tag ($k1 a3 a1) "2")
                )
              )
              (forall ((a4 bool) (true))
                (forall ((_ Unit) ($k1 a4 a1))
                  (and
                    (tag (a4 = true) "3")
                    (tag ($k2 a1 a1 a4) "4")
                    (forall ((a5 int) (a5 = (if (a1 + 1) < 10 then a1 + 1 else 10)))
                      (tag ($k0 a5) "5")
                    )
                  )
                )
              )
            )
          )
        )
      )
    )
  )
)

If I simplify the assert to assert(x >= 2) (or I split the assert in two), scrape does work. This is the constraint for the simplified assert.

(fixpoint "--scrape=both")

(data Unit 0 = [| Unit { }])
(var $k0 ((int))) // orig: $k0
(var $k1 ((int) (int))) // orig: $k1

(constraint
  (and
    (forall ((a0 int) (a0 = 2))
      (tag ($k0 a0) "0")
    )
    (forall ((a1 int) (true))
      (forall ((_ Unit) ($k0 a1))
        (forall ((_ Unit) ((a1 < 10) = true))
          (forall ((_ Unit) (a1 >= 0))
            (and
              (tag ((a1 >= 2) = true) "1")
              (tag ($k1 a1 a1) "2")
              (forall ((a2 int) (a2 = (if (a1 + 1) < 10 then a1 + 1 else 10)))
                (tag ($k0 a2) "3")
              )
            )
          )
        )
      )
    )
  )
)