SMT assertion fails when given function output for tuple comparison

[alberdingk-thijm]

Here's an odd bug that seems to occur when flattening and then encoding certain examples. The below code leads to an assertion failure during execution of SmtUnboxed.encode_exp_z3_single:

type attribute = bool

symbolic failed : option[(int,int)]

let edge_to_int_pair e = match e with
  | 0~1 -> (0, 1)
  | 1~0 -> (1, 0)

let nodes = 2
let edges = {0=1;}

let init n = n = 0n

let trans e x = !(Some (edge_to_int_pair e) = failed) && x

let merge n x y = x || y

let sol = solution { init = init; trans = trans; merge = merge; }

assert foldNodes (fun u v acc -> acc && v) sol true

The source of the error seems to be that encode_exp_z3_single is given an expression ! ((true,0u32,1u32) = (symbolic-failed-proj-0~76,symbolic-failed-proj-1~77,symbolic-failed-proj-2~78)) && x~68, which it can't handle. Note that the tuple comparison in this expression should have been flattened into component comparisons, but for whatever reason, that has not happened here.

The error does not occur when the trans function is written out as:

let trans e x =
  let pair = edge_to_int_pair e in
  !(Some pair = failed) && x