dequantification transformation introduces unsoundness
With the following bomb.mlw
:
axiom test:
forall x:int.
(let y = (not x = 42) in true)
goal foo: false
If we run for example why3 prove bomb.mlw -P CVC5,1.0.4
we correctly get Prover result is: Unknown (sat)
.
However running:
why3 prove bomb.mlw -P CVC5,1.0.4 -a dequantification
gives
File "example.mlw", line 5, characters 10-15:
Goal foo.
Prover result is: Valid (0.01s, 213 steps).