Invalid_argument("List.fold_left2") when trying to get a model

[iguerNL]

command:

./alt-ergo tables-Map-VC_add_max_binding.ae --interpretation last --timelimit 1 --output smtlib2 --timelimit-interpretation 1

File: bug.ae.zip

Output:

 ; Functions
  (define-fun key ((arg_0 (t1, '_c0) tuple2)) t1 k0)
  (define-fun key ((arg_0 (t1, '_c892) tuple2)) t1 !k54)
  (define-fun Tuple2_proj_1 ((arg_0 (t1, '_c0) tuple2)) t1 k0)
  (define-fun Tuple2_proj_1 ((arg_0 (t1, '_c892) tuple2)) t1 !k54)
  (define-fun field ((arg_0 (t3 '_c0 ))) (t2 '_c0 ) !k116)
  (define-fun singleton ((arg_0 (t1, '_c0) tuple2)) (seq (t1, '_c0) tuple2 ) (ite (= arg_0 {Tuple2_proj_1 = k0; Tuple2_proj_2 = v1}) !k134 !k131))
  (define-fun seq_model ((arg_0 (tree '_c0 ))) (seq (t1, '_c0) tuple2 ) !k43)
  (define-fun seq1 ((arg_0 '_c0  m)) (seq (t1, '_c0) tuple2 ) !k43)
  (define-fun repr ((arg_0 (t2 '_c0 ))) (tree '_c0 ) !k122)
  (define-fun Tuple2_proj_2 ((arg_0 (t1, '_c0) tuple2)) '_c0 (ite (= arg_0 {Tuple2_proj_1 = k0; Tuple2_proj_2 = v1}) v1 !k34))
  (define-fun fc ((arg_0 (t3 '_c0 ))) (Array t1 '_c0) !k120)
  (define-fun func ((arg_0 '_c0  m2)) (Array t1 (t1, '_c0) tuple2) !k118)
  (define-fun func ((arg_0 '_c892  m2)) (Array t1 (t1, '_c892) tuple2) !k196)
  (define-fun domn ((arg_0 '_c0  m2)) (Array t1 Bool) !k117)
  (define-fun domn ((arg_0 '_c876  m2)) (Array t1 Bool) !k191)
  (define-fun domn ((arg_0 '_c878  m2)) (Array t1 Bool) !k203)
  (define-fun domn ((arg_0 '_c884  m2)) (Array t1 Bool) !k201)
  (define-fun domn ((arg_0 '_c886  m2)) (Array t1 Bool) !k199)
  (define-fun domn ((arg_0 '_c888  m2)) (Array t1 Bool) !k197)
  (define-fun domn1 ((arg_0 '_c898  m4)) (Array t1 Bool) !k209)
  (define-fun domn1 ((arg_0 '_c914  m4)) (Array t1 Bool) !k212)
  (define-fun result1 ((arg_0 (t1, '_c0) tuple2)) (Array Int (t1, '_c0) tuple2) (ite (= arg_0 (get (mixfix_lb_dtdtrb (seq1 (m1 (field result6))),1),(- (- (card (m3 result6)) 1) 1))) !k159 !k135))
  Fatal error: exception Invalid_argument("List.fold_left2")

[iguerNL]

Here is smaller example that triggers the bug:

type t
type r = { domn : bool ; card : int }
logic a : t
logic b : r
logic f : t -> r


(* no failure if f(a) is replaced by b *)
goal g_18 :
  (f(a)).domn ->
  false

[bclement-ocp]

There are two compounding bugs here:

• First, in check_records, we assume that any function that returns a record is a record constructor (and any function of one argument taking a record is a record destructor, although I don't think this actually has an adverse impact except in terms of performance). This is the cause of the crash.

• Second, we do not properly keep track of accesses. f(a) is normalized to some constant (say, !k3) by purification, but we only see accesses to f(a).domn as a term, not to !k3.domn, so although we have both the informations that f(a) = !k3 and f(a).domn = true, we don't know that !k3.domn = true.

This is somewhat related to #792 and #793 . A proper fix would probably require re-architecturing at least partially the model generation for record and will have to wait until #776 is merged.

[Halbaroth]

The bug is not present anymore. The current output for the above file is:

(
  (define-fun a () t (as @a3 t))
  (define-fun b () r (as @a1 r))
  (define-fun f ((_arg_0 t)) r (r true 0))
)

which is a correct counter example (the goal becomes true -> false).

Alt-Ergo outputs Valid on the original file. As we do not print anymore models after a timeout, I cannot check if the bug is still there for this file but I believe that it is gone :)