This code fails to encode into SMT after partially evaluating with the following error:

Code

(* This example causes an SMT unboxing error.
 * It does not occur when there is only one field.
 *)

type rec = { foo: option[int]; bar: bool }
type attribute = rec

let nodes = 2

let edges = {
  0=1;
}

let trans e a = match a with
  | { foo = f; _ } -> match f with
    | Some y -> { foo = Some (y + 1); bar = true }
    | _ -> a

let merge n x y = match (x, y) with
  | ({ foo = Some x1; _ }, { foo = Some y1; _ }) -> if x1 < y1 then x else y
  | ({ foo = None; _ }, _ ) -> y
  | (_, { foo = None; _ }) -> x

let init n = match n with
  | 0n -> { foo = Some 0; bar = true }
  | 1n -> { foo = None; bar = false }

let assert node x = !(x.foo = None) && x.bar = true

Error

Fatal error: exception Failure("internal error (check that tuples are flat)")
Raised at file "pervasives.ml", line 32, characters 17-33
Called from file "src/lib/smt/SmtUnboxed.ml", line 193, characters 20-53
Called from file "src/lib/smt/SmtUnboxed.ml", line 175, characters 19-52
Called from file "src/lib/smt/SmtUnboxed.ml", line 167, characters 20-53
Called from file "src/lib/smt/SmtUnboxed.ml", line 291, characters 15-47
Called from file "src/lib/smt/SmtClassicEncoding.ml", line 152, characters 20-45
Called from file "src/lib/smt/SmtClassicEncoding.ml", line 270, characters 12-68
Called from file "src/lib/smt/Smt.ml", line 142, characters 29-42
Called from file "src/lib/utils/Profile.ml", line 10, characters 12-16
Called from file "src/lib/smt/Smt.ml", line 141, characters 6-204
Called from file "src/lib/smt/Smt.ml", line 179, characters 12-24
Called from file "src/lib/Main_defs.ml", line 94, characters 10-60
Called from file "src/lib/utils/Profile.ml", line 10, characters 12-16
Called from file "src/lib/Main_defs.ml", line 136, characters 8-161
Called from file "src/exe/Main.ml", line 22, characters 12-37
Called from file "src/lib/utils/Profile.ml", line 10, characters 12-16
Called from file "src/exe/Main.ml", line 32, characters 2-67

Deleting the bar field (and references to it) makes the code work.

NetworkVerification / nv

SMT unboxing bug when handling multi-field records #45

Code

Error