inconsistency after axiom instantiations for the 'nat' theory with redux solver

[necto]

Here is a simple lemma to verify with the latest version ( #d8d505f ) master of verifast:

//@ #include <nat.gh>

/*@
  lemma void some_lemma(nat from, nat to)
  requires succ(from) != to;
  ensures true;
  {
    if (int_of_nat(succ(from)) == int_of_nat(to)) {
      assert(nat_of_int(int_of_nat(succ(from))) ==
              nat_of_int(int_of_nat(to)));
    }
  }
  @*/

I get a weird message for the assert:
redux: INFO: Detected an inconsistency after axiom instantiations triggered by the construction of new terms (rather than after adding a new assumption). This might indicate an inconsistency in the axioms. Call 'verifast -verbose 10' to diagnose.

Here is the -verbose 10 output: log.txt
Unfortunately these messages did not clarified the picture.

What is the inconsistency here, and how to eliminate it?

[btj]

This is a false alarm. Semantically, the inconsistency in the path condition is introduced by assuming that the if condition is true, but Redux doesn't notice the inconsistency at that point. It notices the inconsistency only when the terms nat_of_int(int_of_nat(succ(from))) and nat_of_int(int_of_nat(to)) are constructed, which trigger the int_of_nat_of_int auto-lemma declared in nat.gh. This is perfectly fine.

The inconsistency is intended: you are doing a proof by contradiction.

Arguably, having Redux generate this message was a bad idea.