ivy/test/mc4.ivy

#lang ivy1.7

type t

var x : t
var y : t


axiom X:t = 0 & Y = 0 -> X = Y
axiom X:t = Y & Y = 0 -> X = 0

invariant x = y

after init {
    x := 0;
    y := 0
}

action a  = {
  x := 0
}


export a