Pattern matching with record leads to a crash for CVC4 & Z3
The encoding that is done for the pattern matching for cvc4 and z3 looks to be unsupported by the provers when a record is destructed in the pattern matching. Look at the example bellow.
use int.Int
type t = { a : int; b : int }
type s = X t | Y
predicate f (x : s) =
match x with
| Y -> false
| X { a = a; b = b } -> a > 0 /\ b > 0
| X _ -> false
end
lemma L: f (X { a = 42; b = 42})
With why3 prove -P CVC4,1.8 a.mlw
, I get
File "test.mlw", line 15, characters 2-24:
Goal L.
Prover result is: High failure (0.01s, 8 steps),
Prover exit status: exited with status 1
prove output:
(error "Parse Error: /tmp/why_9dbac4_a-T-L.smt2:25.74: Symbol 'tqtmk_proj_1' not declared as a variable
...x1 (X_proj_1 x))) (let ((x2 (tqtmk_proj_1 x1))
^
")
The same error happens with Z3 too.