SMT unboxing bug when handling multi-field records
alberdingk-thijm opened this issue · 1 comments
alberdingk-thijm commented
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.
DKLoehr commented
What's happening here is that tuple flattening is supposed to unroll tuple equalities, but fails to do that when one of the sides is surrounded by a TGet. Will fix soon.