Strange "z3 exception"

[steinwaywhw]

Suppose we have the following definitions and test files,

sortdef elt = int

stacst elt_eq: (elt, elt) -> bool 
stadef == = elt_eq 

praxi lemma_eq_elt {e:elt} (): [e == e] unit_p

datasort seq = 
| seq_empty of ()
| seq_more of (elt, seq)

stadef nil = seq_empty
stadef :: = seq_more

stacst seq_head: seq -> elt 
stacst seq_tail: seq -> seq
stacst seq_eq: (seq, seq) -> bool

stadef head = seq_head
stadef tail = seq_tail
stadef ==  = seq_eq

praxi lemma_eq_seq_id {g:seq} (): [g == g] unit_p
praxi lemma_eq_seq_sym {g1,g2:seq|g1 == g2} (): [g2 == g1] unit_p
praxi lemma_eq_seq_trans {g1,g2,g3:seq|g1 == g2 && g2 == g3} (): [g1 == g3] unit_p

praxi lemma_head {e:elt} {g:seq} (): [head(e \seq_more g) == e] unit_p
//praxi lemma_tail {e:elt} {g:seq} (): [tail(e::g) == g] unit_p

And this,

local 


val _ = $solver_assert (lemma_eq_elt)

val _ = $solver_assert (lemma_eq_seq_id)
val _ = $solver_assert (lemma_eq_seq_sym)
val _ = $solver_assert (lemma_eq_seq_trans)

val _ = $solver_assert (lemma_head)
//val _ = $solver_assert (lemma_tail)

abstype seq (seq)

extern fun test1 (): seq (1 :: 2 :: nil)
extern fun test2 (): seq (1 :: 2 :: nil)
extern fun require_eq {g1,g2:seq|head(g1) == 1} (seq g1, seq g2): void 

in 


val a = test1()
val b = test2()
val _ = require_eq (a, b)

end

It will throw z3_exception, but this is indeed very similar to ilist defined by Hongwei.

[steinwaywhw]

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/extsolve/SATS/ilist.sats