VerCors crash should be more informative if crash is caused by unsound axiom being added

[bobismijnnaam]

Crash Message

An error condition was reached, which should be statically unreachable. `requires true` is always satisfiable.. Inner failure:
 > ======================================
 > At test.pvl
 > --------------------------------------
 >    14  }
 >    15  
 >       [-----------
 >    16  class C {
 >    17    
 >    18  }
 >        -]
 >    19  
 >    20  void m() {
 > --------------------------------------
 > The precondition of this contract may be unsatisfiable. If this is intentional, replace it with `requires false`. (https://utwente.nl/vercors#unsatisfiable)
 > ======================================
  at vct.col.origin.PanicBlame.blame(Blame.scala:1415)
  at vct.col.rewrite.CheckContractSatisfiability$AssertPassedNontrivialUnsatisfiable.blame(CheckContractSatisfiability.scala:48)
  at vct.col.rewrite.CheckContractSatisfiability$AssertPassedNontrivialUnsatisfiable.blame(CheckContractSatisfiability.scala:40)
  at vct.col.origin.ExpectedError.signalDone(ExpectedError.scala:32)
  at vct.main.stages.ExpectedErrors.$anonfun$run$1(ExpectedErrors.scala:16)
  at vct.main.stages.ExpectedErrors.$anonfun$run$1$adapted(ExpectedErrors.scala:16)
  at scala.collection.immutable.List.foreach(List.scala:333)
  at vct.main.stages.ExpectedErrors.run(ExpectedErrors.scala:16)
  at vct.main.stages.ExpectedErrors.run(ExpectedErrors.scala:12)
  at hre.stages.Stages.$anonfun$run$3(Stages.scala:104)
  at hre.stages.Stages.$anonfun$run$3$adapted(Stages.scala:101)
  at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
  ...
  at vct.main.Main$.main(Main.scala:50)
  at vct.main.Main.main(Main.scala)

Version Information

• VerCors version 9999.9.9-SNAPSHOT
• At commit dc107f0 from branch dev (changes=false)

Arguments

test.pvl --backend-file-base temp

File Inputs

test.pvl

// enum MyEnum {

// }

adt MyAdt {
  pure int my_enum1(MyAdt myEnum1);

  pure int one();
  pure int two();

  axiom one() == 1 && two() == 2;

  axiom one() == two();
}

class C {
  
}

void m() {
  assert false;
}

Full Log

13:20:53.445 [INFO] Start: VerCors (at 13:20:53)
13:20:59.395 [INFO] Done: VerCors (at 13:20:59, duration: 00:00:05)
13:20:59.401 [ERROR] vct.col.origin.BlameUnreachable: An error condition was reached, which should be statically unreachable. `requires true` is always satisfiable.. Inner failure:
 > ======================================
 > At test.pvl
 > --------------------------------------
 >    14  }
 >    15  
 >       [-----------
 >    16  class C {
 >    17    
 >    18  }
 >        -]
 >    19  
 >    20  void m() {
 > --------------------------------------
 > The precondition of this contract may be unsatisfiable. If this is intentional, replace it with `requires false`. (https://utwente.nl/vercors#unsatisfiable)
 > ======================================
	at vct.col.origin.PanicBlame.blame(Blame.scala:1415)
	at vct.col.rewrite.CheckContractSatisfiability$AssertPassedNontrivialUnsatisfiable.blame(CheckContractSatisfiability.scala:48)
	at vct.col.rewrite.CheckContractSatisfiability$AssertPassedNontrivialUnsatisfiable.blame(CheckContractSatisfiability.scala:40)
	at vct.col.origin.ExpectedError.signalDone(ExpectedError.scala:32)
	at vct.main.stages.ExpectedErrors.$anonfun$run$1(ExpectedErrors.scala:16)
	at vct.main.stages.ExpectedErrors.$anonfun$run$1$adapted(ExpectedErrors.scala:16)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at vct.main.stages.ExpectedErrors.run(ExpectedErrors.scala:16)
	at vct.main.stages.ExpectedErrors.run(ExpectedErrors.scala:12)
	at hre.stages.Stages.$anonfun$run$3(Stages.scala:104)
	at hre.stages.Stages.$anonfun$run$3$adapted(Stages.scala:101)
	at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
	at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
	at scala.collection.AbstractIterable.foreach(Iterable.scala:933)
	at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:903)
	at hre.stages.Stages.$anonfun$run$1(Stages.scala:101)
	at hre.progress.task.NameSequenceTask.scope(NameSequenceTask.scala:16)
	at hre.progress.Progress$.stages(Progress.scala:47)
	at hre.stages.Stages.run(Stages.scala:98)
	at hre.stages.Stages.run$(Stages.scala:95)
	at hre.stages.StagesPair.run(Stages.scala:145)
	at vct.main.modes.Verify$.verifyWithOptions(Verify.scala:64)
	at vct.main.modes.Verify$.$anonfun$runOptions$3(Verify.scala:99)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.util.Time$.logTime(Time.scala:23)
	at vct.main.modes.Verify$.runOptions(Verify.scala:99)
	at vct.main.Main$.runMode(Main.scala:107)
	at vct.main.Main$.$anonfun$runOptions$3(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.middleware.Middleware$.using(Middleware.scala:78)
	at vct.main.Main$.$anonfun$runOptions$2(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.io.Watch$.booleanWithWatch(Watch.scala:58)
	at vct.main.Main$.$anonfun$runOptions$1(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.middleware.Middleware$.using(Middleware.scala:78)
	at vct.main.Main$.runOptions(Main.scala:95)
	at vct.main.Main$.main(Main.scala:50)
	at vct.main.Main.main(Main.scala)

13:20:59.402 [ERROR] !*!*!*!*!*!*!*!*!*!*!*!
13:20:59.402 [ERROR] ! VerCors has crashed !
13:20:59.402 [ERROR] !*!*!*!*!*!*!*!*!*!*!*!
13:20:59.402 [ERROR] Please report this as a bug here: