Wrong bound generation for definition of "even"

[Joachim Jansen]

The definition

    {
        even(0).
        !t: even(t) <- even(t-2).
    }

leads to a wrong CT bound:

BEFORE PROPAGATION: structure  : V {
  x = { 0..4 }
  even<ct> = {  }
  even<cf> = {  }
}

**   Applying propagation for even
    Old interpretation was<ct>: {}
    <cf>: {}

    The used BDDs are:
    CT: 
    EXISTS(var779[s-2..2]) {
        =(+(+(-2[int],*(-1[int],var779[s-2..2])),var596[x]),0[nat])
            FALSE BRANCH:
                false
            TRUE BRANCH:
                true
    }
        FALSE BRANCH:
            true
        TRUE BRANCH:
            EXISTS(var780[s-2..2]) {
                EXISTS(var781[s-2..2]) {
                    =(+(+(-2[int],*(-1[int],var781[s-2..2])),var780[s-2..2]),0[nat])
                        FALSE BRANCH:
                            false
                        TRUE BRANCH:
                            true
                }
                    FALSE BRANCH:
                        false
                    TRUE BRANCH:
                        =(+(+(-2[int],*(-1[int],var780[s-2..2])),var596[x]),0[nat])
                            FALSE BRANCH:
                                false
                            TRUE BRANCH:
                                true
            }
                FALSE BRANCH:
                    true
                TRUE BRANCH:
                    false

    CF:  ... (not interesting)

    Derived symbols: <ct>: {(0); (1)}
    <cf>: {}

    Result: <ct>: {(0); (1)}
    <cf>: {}
**

The Bound basically says (when generating var596 of type x [0..4]):

1: If I can't find a variable v'[-2..2] such that var596 - 2 = v', I succeed
   (this will never happen)
2: Otherwise, try to find a tuple of variables v' and v'' 
    (both of type [-2,2]), such that 
       v596 - 2 = v'
       v' - 2 = v''
    both hold.
    If I can't find such a tuple, the bound succeeds as well.

This leads to generation of v596 = {0;1}, when the domain element 1 should not be derived to be certainly true for the definition given above.

This bug does not occur on the master branch, because the old implementation of pushing quantifiers will cause other formulas to be sent to the bounds creator. The bounds generation is correct for the current pushed form:

(! var344[x] : (~=(var344[x],0) | ~x(0) | even(var344[x])))

but not for the 'new' pushed form:

(~x(0) | (! var344[x] : (~=(var344[x],0) | even(var344[x]))))

[Joachim Jansen]

Additional information: the (correct) bound when generating a bound for the 'old' pushed form of

(! var344[x] : (~=(var344[x],0) | ~x(0) | even(var344[x])))

is the following:

    CT: 
    EXISTS(var731[s-2..2]) {
        =(+(+(-2[int],*(-1[int],var731[s-2..2])),var596[x]),0[nat])
            FALSE BRANCH:
                false
            TRUE BRANCH:
                true
    }
        FALSE BRANCH:
            true
        TRUE BRANCH:
            =(var596[x],0[nat])
                FALSE BRANCH:
                    false
                TRUE BRANCH:
                    EXISTS(var732[sort350]) {
                        =(var732[sort350],0[nat])
                            FALSE BRANCH:
                                false
                            TRUE BRANCH:
                                x(var732[sort350])
                                    FALSE BRANCH:
                                        true
                                    TRUE BRANCH:
                                        false
                    }
                        FALSE BRANCH:
                            true
                        TRUE BRANCH:
                            EXISTS(var733[sort350]) {
                                =(var733[sort350],0[nat])
                                    FALSE BRANCH:
                                        false
                                    TRUE BRANCH:
                                        true
                            }
                                FALSE BRANCH:
                                    true
                                TRUE BRANCH:
                                    false