Revealed axiom doesn't make it to SMT solver

[RustanLeino]

Dafny version

4.10.1

Code to produce this issue

datatype Cell = Cell(k: int)

function MakeCell(x: int): Cell {
  Cell(x)
}

lemma Test(x: int)
{
  hide MakeCell;

  calc {
    MakeCell(x);
  ==  { reveal MakeCell(); } // this calc step gives an error, despite the reveal
    Cell(x);
  }

  var something := Cell(x);
}

Command to run and resulting output

% dafny test.dfy /print:test.bpl /proverLog:direct-from-dafny.smt2
Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
test.dfy(16,8): Error: the calculation step between the previous line and this line could not be proved

Dafny program verifier finished with 0 verified, 1 error

% boogied test.bpl /proverLog:starting-from-boogie.smt2

Boogie program verifier finished with 1 verified, 0 errors

What happened?

Running Dafny to verify to program above fails, but it ought to succeed.

Looking into this a bit further, I generate test.bpl from the Dafny program and run Boogie on test.bpl. (In the repro I show above, boogied is a local script that invokes boogie with the options that Dafny passes to it, to the best of my understanding.) Running Boogie directly on test.bpl, the verification succeeds!

I've compared the /proverLog generated when running Dafny and when running Boogie. The one difference (other than reordering of some things, which I straightened out locally) is that the axiom

(assert (forall ((|x#0| Int) ) (!  (=> (|_module.__default.MakeCell#canCall| |x#0|) (= (_module.__default.MakeCell |x#0|) (|#_module.Cell.Cell| |x#0|)))
 :pattern ( (_module.__default.MakeCell |x#0|))
)))

is included when running Boogie directly but not when running Dafny. This axiom is what's needed to verify the original Dafny program. So, it seems that Boogie somehow does not include this axiom when running Dafny.

What type of operating system are you experiencing the problem on?

Mac