Counterexample extraction fails due to Boogie

[aterga]

Asking Carbon to produce counterexamples for the following program results in a crash:

function hello(x: Int): Int
method problematic() {
	var x: Int
	assert x == hello(x);
}

When running with options --counterexample variables, the trace looks like this:

      scala.None$.get(Option.scala:349)
      scala.None$.get(Option.scala:347)
      viper.carbon.boogie.BoogieModelTransformer$.transformCounterexample(BoogieModelTransformer.scala:20)
      viper.carbon.CarbonVerifier.$anonfun$verify$3(CarbonVerifier.scala:202)
      viper.carbon.CarbonVerifier.$anonfun$verify$3$adapted(CarbonVerifier.scala:202)
      scala.collection.Iterator.foreach(Iterator.scala:937)
      scala.collection.Iterator.foreach$(Iterator.scala:937)
      scala.collection.AbstractIterator.foreach(Iterator.scala:1425)
      scala.collection.IterableLike.foreach(IterableLike.scala:70)
      scala.collection.IterableLike.foreach$(IterableLike.scala:69)
      scala.collection.AbstractIterable.foreach(Iterable.scala:54)
      viper.carbon.CarbonVerifier.verify(CarbonVerifier.scala:202)

Switching to ``--counterexample native``` results in

Internal error: An internal error occurred. Found an unparsable output from Boogie: Prover error: Model parsing error: Invalid model: invalid element name 1.0, at line 3 (FullPerm -> 1.0) (<no position>)
Internal error: An internal error occurred. Found an unparsable output from Boogie: Prover error: Could not parse any models (<no position>)
Internal error: An internal error occurred. Found 3 errors, but there should be 1. The output was: Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.\nProver error: Model parsing error: Invalid model: invalid element name 1.0, at line 3 (FullPerm -> 1.0)\nProver error: Could not parse any models\n  Assert might fail. Assertion x == hello(x) might not hold. ([email protected]) [5]\n\nBoogie program verifier finished with 1 verified, 1 error\n (<no position>)

Silicon manages to produce counterexamples for both values of --counterexample.