struct bug

[gipsyh]

#lang ivy1.7

type ttt = struct {
    a: bool
}

type x_t

interpret x_t -> int

function xx(X: x_t): ttt

after init {
    a(xx(0)) := false;
    a(xx(1)) := true;
}

invariant ~a(xx(0))

this invariant should be hold but ivy_check not

Isolate this:

    The inductive invariant consists of the following conjectures:
        test.ivy: line 18: invar3

    The following initializers are present:
        test.ivy: line 13: init[after2]

    Initialization must establish the invariant
        test.ivy: line 18: invar3 ... FAIL
searching for a small model... done
[
    a(1) = true
    a(0) = false
    1:x_t = 1
    0:x_t = 0
]
init

{
test.ivy: line 14: 
    a(xx(0)) := false

    [
        xx(1) = 0
        xx(0) = 0
    ]
test.ivy: line 15: 
    a(xx(1)) := true

    [
        xx(1) = 1
        xx(0) = 1
    ]
}

[glycerine]

The solver is free to choose xx(1) equal to xx(0) since xx is an uninterpreted function, and thus your assignment "a(xx(1)) := true" also made "a(xx(0)) := true", which violates the invariant.

If, in the after init block, you had done the assignment of false 2nd (last) -- after the assignment of true, then the invariant would hold.

But either way the conceptual missing piece is that the range of xx could have a size of 1.