Unexpected behavior with a macro inside an if statement

[hidenori-shinohara]

The following code throws a CTI with my_obj.always_false_macro(0) = true in the pre-state, which doesn't make much sense.

#lang ivy1.7

type my_type

object my_obj =  {
    relation relation_that_we_never_update(SOMETHING:my_type)

    after init {
        relation_that_we_never_update(X) := true;
    }

    relation always_false_macro(SOMETHING:my_type)
    definition always_false_macro(something:my_type) = false

    action my_action_macro(something:my_type) = {
        if (always_false_macro(something)) {
            # We should never get here because `always_false_macro` is always false.
            # But Ivy seems to get confused and think that this is reachable.
            relation_that_we_never_update(something) := false;
        }
    }
}


# This should always be true since
# (1) We set relation_that_we_never_update to be `true` in the initialization.
# (2) We never update this relation.
invariant forall X. my_obj.relation_that_we_never_update(X)

export my_obj.my_action_macro

[nano-o]

It seems to me that macros are only unfolded in assertions and invariants, but not when used in other statements.