Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3

configure.in

@@ -495,8 +495,10 @@ else
         COQVERSION=`$COQC -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
 
         #Even if the name of the variable is CAMLP4 the value can be camlp5
-        COQCAMLP=$(eval `coqtop -config`; echo ${CAMLP4BIN}${CAMLP4}o)
-        COQCAMLPLIB=$(eval `coqtop -config`; echo ${CAMLP4LIB})
+        CAMLP4BIN=`coqtop -config | sed -n -e 's/CAMLP4BIN=\(.*\)$/\1/p'`
+        CAMLP4=`coqtop -config | sed -n -e 's/CAMLP4=\(.*\)$/\1/p'`
+        COQCAMLPLIB=`coqtop -config | sed -n -e 's/CAMLP4LIB=\(.*\)$/\1/p'`
+        COQCAMLP=${CAMLP4BIN}${CAMLP4}o
 
         case $COQVERSION in
           8.4*)

examples/vstte12_ring_buffer.mlw

@@ -139,3 +139,85 @@ module Harness
     let h = pop b in assert { h = z }
 
 end
+
+(** With sequences instead of lists *)
+
+module RingBufferSeq
+
+  use import int.Int
+  use import seq.Seq as S
+  use import array.Array
+
+  type buffer 'a = {
+    mutable first: int;
+    mutable len  : int;
+            data : array 'a;
+    ghost mutable sequence: S.seq 'a;
+  }
+  invariant {
+    let size = Array.length self.data in
+    0 <= self.first <  size /\
+    0 <= self.len   <= size /\
+    self.len = S.length self.sequence /\
+    forall i: int. 0 <= i < self.len ->
+      (self.first + i < size ->
+         S.([]) self.sequence i = self.data[self.first + i]) /\
+      (0 <= self.first + i - size ->
+         S.([]) self.sequence i = self.data[self.first + i - size])
+  }
+
+  (* total capacity of the buffer *)
+  function size (b: buffer 'a) : int = Array.length b.data
+
+  (* length = number of elements *)
+  function length (b: buffer 'a) : int = b.len
+
+  (* code *)
+
+  let create (n: int) (dummy: 'a) : buffer 'a
+    requires { n > 0 }
+    ensures  { size result = n }
+    ensures  { result.sequence = S.empty }
+  = { first = 0; len = 0; data = make n dummy; sequence = S.empty }
+
+  let length (b: buffer 'a) : int
+    ensures { result = length b }
+  = b.len
+
+  let clear (b: buffer 'a) : unit
+    writes  { b.len, b.sequence }
+    ensures { length b = 0 }
+    ensures { b.sequence = S.empty }
+  = ghost b.sequence <- S.empty;
+    b.len <- 0
+
+  let push (b: buffer 'a) (x: 'a) : unit
+    requires { length b < size b }
+    writes   { b.data.elts, b.len, b.sequence }
+    ensures  { length b = (old (length b)) + 1 }
+    ensures  { b.sequence = S.snoc (old b.sequence) x }
+  = ghost b.sequence <- S.snoc b.sequence x;
+    let i = b.first + b.len in
+    let n = Array.length b.data in
+    b.data[if i >= n then i - n else i] <- x;
+    b.len <- b.len + 1
+
+  let head (b: buffer 'a) : 'a
+    requires { length b > 0 }
+    ensures  { result = S.([]) b.sequence 0 }
+  = b.data[b.first]
+
+  let pop (b: buffer 'a) : 'a
+    requires { length b > 0 }
+    writes   { b.first, b.len, b.sequence }
+    ensures  { length b = (old (length b)) - 1 }
+    ensures  { result = S.([]) (old b.sequence) 0 }
+    ensures  { b.sequence = (old b.sequence)[1 ..] }
+  = ghost b.sequence <- b.sequence[1 ..];
+    let r = b.data[b.first] in
+    b.len <- b.len - 1;
+    let n = Array.length b.data in
+    b.first <- b.first + 1;
+    if b.first = n then b.first <- 0;
+    r
+end

src/mlw/dexpr.mli

@@ -97,7 +97,8 @@ and dexpr_node =
   | DElet of dlet_defn * dexpr
   | DErec of drec_defn * dexpr
   | DEnot of dexpr
-  | DElazy of lazy_op * dexpr * dexpr
+  | DEand of dexpr * dexpr
+  | DEor of dexpr * dexpr
   | DEif of dexpr * dexpr * dexpr
   | DEcase of dexpr * (dpattern * dexpr) list
   | DEassign of (dexpr * rsymbol * dexpr) list
@@ -157,4 +158,4 @@ val drec_defn : denv -> pre_fun_defn list -> denv * drec_defn
 val expr : ?keep_loc:bool -> dexpr -> expr
 
 val let_defn : ?keep_loc:bool -> dlet_defn -> let_defn
-val rec_defn : ?keep_loc:bool -> drec_defn -> rec_defn
+val rec_defn : ?keep_loc:bool -> drec_defn -> let_defn

src/mlw/expr.mli

@@ -19,7 +19,6 @@ open Ity
 type rsymbol = private {
   rs_name  : ident;
   rs_cty   : cty;
-  rs_ghost : bool;
   rs_logic : rs_logic;
   rs_field : pvsymbol option;
 }
@@ -64,6 +63,8 @@ val create_field : preid -> itysymbol -> pvsymbol -> rsymbol
 val restore_rs : lsymbol -> rsymbol
 (** raises [Not_found] if the argument is not a [rs_logic] *)
 
+val rs_ghost : rsymbol -> bool
+
 (** {2 Program patterns} *)
 
 type prog_pattern = private {
@@ -86,8 +87,6 @@ val create_prog_pattern :
 
 (** {2 Program expressions} *)
 
-type lazy_op = Eand | Eor
-
 type assertion_kind = Assert | Assume | Check
 
 type for_direction = To | DownTo
@@ -100,130 +99,119 @@ type variant = term * lsymbol option (** tau * (tau -> tau -> prop) *)
 
 type assign = pvsymbol * rsymbol * pvsymbol (* region * field * value *)
 
-type vty =
-  | VtyI of ity
-  | VtyC of cty
-
-type val_decl =
-  | ValV of pvsymbol
-  | ValS of rsymbol
-
 type expr = private {
   e_node   : expr_node;
-  e_vty    : vty;
-  e_ghost  : bool;
+  e_ity    : ity;
   e_effect : effect;
-  e_vars   : Spv.t;
-  e_syms   : Srs.t;
   e_label  : Slab.t;
   e_loc    : Loc.position option;
 }
 
 and expr_node = private
   | Evar    of pvsymbol
-  | Esym    of rsymbol
   | Econst  of Number.constant
-  | Eapp    of expr * pvsymbol list * cty
-  | Efun    of expr
+  | Eexec   of cexp
+  | Eassign of assign list
   | Elet    of let_defn * expr
-  | Erec    of rec_defn * expr
-  | Enot    of expr
-  | Elazy   of lazy_op * expr * expr
   | Eif     of expr * expr * expr
   | Ecase   of expr * (prog_pattern * expr) list
-  | Eassign of assign list
   | Ewhile  of expr * invariant list * variant list * expr
   | Efor    of pvsymbol * for_bounds * invariant list * expr
   | Etry    of expr * (xsymbol * pvsymbol * expr) list
   | Eraise  of xsymbol * expr
-  | Eghost  of expr
   | Eassert of assertion_kind * term
   | Epure   of term
   | Eabsurd
-  | Etrue
-  | Efalse
-  | Eany
 
-and let_defn = private {
-  let_sym  : val_decl;
-  let_expr : expr;
+and cexp = private {
+  c_node : cexp_node;
+  c_cty  : cty;
 }
 
+and cexp_node = private
+  | Capp of rsymbol * pvsymbol list
+  | Cfun of expr
+  | Cany
+
+and let_defn = private
+  | LDvar of pvsymbol * expr
+  | LDsym of rsymbol * cexp
+  | LDrec of rec_defn list
+
 and rec_defn = private {
-  rec_defn : fun_defn list;
-  rec_decr : lsymbol option;
+  rec_sym  : rsymbol; (* exported symbol *)
+  rec_rsym : rsymbol; (* internal symbol *)
+  rec_fun  : cexp;    (* Cfun *)
+  rec_varl : variant list;
 }
 
-and fun_defn = {
-  fun_sym  : rsymbol; (* exported symbol *)
-  fun_rsym : rsymbol; (* internal symbol *)
-  fun_expr : expr;    (* Efun *)
-  fun_varl : variant list;
-}
+(** {2 Expressions} *)
 
 val e_label : ?loc:Loc.position -> Slab.t -> expr -> expr
 val e_label_add : label -> expr -> expr
 val e_label_copy : expr -> expr -> expr
 
-exception ItyExpected of expr
-exception CtyExpected of expr
+val e_ghost : expr -> bool
+val c_ghost : cexp -> bool
 
-val ity_of_expr : expr -> ity
-val cty_of_expr : expr -> cty
+val e_ghostify : bool -> expr -> expr
+val c_ghostify : bool -> cexp -> cexp
 
-val check_expr : expr -> unit
-(** [check_expr e] verifies that [e] does not perform bad
-    ghost writes nor contains stale (i.e., reset) regions.
-    This function must be called for any expression which
-    is used outside of an [Efun]-closure. *)
+(** {2 Definitions} *)
 
-val e_fold : ('a -> expr -> 'a) -> 'a -> expr -> 'a
+val let_var :
+  preid -> ?ghost:bool -> expr -> let_defn * pvsymbol
 
-val e_find_minimal : (expr -> bool) -> expr -> expr
-(** [e_find_minimal pr e] looks for a minimal sub-expression
-    of [e] satisfying [pr], raises [Not_found] if none found. *)
+val let_sym :
+  preid -> ?ghost:bool -> ?kind:rs_kind -> cexp -> let_defn * rsymbol
 
-val proxy_label : label
+val let_rec :
+  (rsymbol * cexp * variant list * rs_kind) list -> let_defn * rec_defn list
 
-(** {2 Smart constructors} *)
+(** {2 Callable expressions} *)
 
-val e_var : pvsymbol -> expr
-val e_sym : rsymbol  -> expr
+val c_app : rsymbol -> pvsymbol list -> ity list -> ity -> cexp
 
-val e_const : Number.constant -> expr
-val e_nat_const : int -> expr
+val c_fun :
+  pvsymbol list -> pre list -> post list -> post list Mexn.t -> expr -> cexp
 
-val create_let_defn_pv :
-  preid -> ?ghost:bool -> expr -> let_defn * pvsymbol
+val c_any : cty -> cexp
+
+type ext_cexp = let_defn list * cexp
 
-val create_let_defn_rs :
-  preid -> ?ghost:bool -> ?kind:rs_kind -> expr -> let_defn * rsymbol
+val ext_c_sym : rsymbol -> ext_cexp
 
-val create_let_defn :
-  preid -> ?ghost:bool -> ?kind:rs_kind -> expr -> let_defn
+val ext_c_app : ext_cexp -> expr list -> ity list -> ity -> ext_cexp
 
-val create_rec_defn :
-  (rsymbol * expr (* Efun *) * variant list * rs_kind) list -> rec_defn
+(** {2 Expression constructors} *)
 
-val e_fun :
-  pvsymbol list -> pre list -> post list -> post list Mexn.t -> expr -> expr
+val e_var : pvsymbol -> expr
+
+val e_const : Number.constant -> expr
+val e_nat_const : int -> expr
+
+val e_exec : cexp -> expr
+
+val e_app : rsymbol -> expr list -> ity list -> ity -> expr
 
 val e_let : let_defn -> expr -> expr
-val e_rec : rec_defn -> expr -> expr
 
-val e_app : expr -> expr list -> ity list -> ity -> expr
+exception FieldExpected of rsymbol
 
 val e_assign : (expr * rsymbol * expr) list -> expr
 
-val e_ghost : expr -> expr
-val e_ghostify : expr -> expr
-
 val e_if : expr -> expr -> expr -> expr
-val e_lazy : lazy_op -> expr -> expr -> expr
+
+val e_and : expr -> expr -> expr
+val e_or  : expr -> expr -> expr
 val e_not : expr -> expr
-val e_true : expr
+
+val e_true  : expr
 val e_false : expr
 
+val is_e_true  : expr -> bool
+val is_e_false : expr -> bool
+
 val e_raise : xsymbol -> expr -> ity -> expr
 
 val e_try : expr -> (xsymbol * pvsymbol * expr) list -> expr
@@ -232,8 +220,8 @@ val e_case : expr -> (prog_pattern * expr) list -> expr
 
 val e_while : expr -> invariant list -> variant list -> expr -> expr
 
-val e_for :
-  pvsymbol -> expr -> for_direction -> expr -> invariant list -> expr -> expr
+val e_for : pvsymbol ->
+  expr -> for_direction -> expr -> invariant list -> expr -> expr
 
 val e_pure : term -> expr
 
@@ -241,15 +229,21 @@ val e_assert : assertion_kind -> term -> expr
 
 val e_absurd : ity -> expr
 
-val e_any : cty -> expr
+(** {2 Expression manipulation tools} *)
 
-(** {2 Built-in symbols} *)
+val e_fold : ('a -> expr -> 'a) -> 'a -> expr -> 'a
+(** [e_fold] does not descend into Cfun *)
+
+val e_locate_effect : (effect -> bool) -> expr -> Loc.position option
+(** [e_locate_effect pr e] looks for a minimal sub-expression of
+    [e] whose effect satisfies [pr] and returns its location *)
 
-val rs_bool_true  : rsymbol
-val rs_bool_false : rsymbol
+val proxy_label : label
+
+(** {2 Built-in symbols} *)
 
-val e_bool_true  : expr
-val e_bool_false : expr
+val rs_true  : rsymbol
+val rs_false : rsymbol
 
 val rs_tuple : int -> rsymbol
 val e_tuple : expr list -> expr
@@ -257,6 +251,7 @@ val e_tuple : expr list -> expr
 val rs_void : rsymbol
 val e_void : expr
 
+val is_e_void : expr -> bool
 val is_rs_tuple : rsymbol -> bool
 
 val rs_func_app : rsymbol
@@ -268,8 +263,7 @@ val e_func_app_l : expr -> expr list -> expr
 val forget_rs  : rsymbol -> unit (* flush id_unique for a program symbol *)
 
 val print_rs   : Format.formatter -> rsymbol -> unit  (* program symbol *)
+
 val print_expr : Format.formatter -> expr -> unit     (* expression *)
 
-val print_val_decl : Format.formatter -> val_decl -> unit
 val print_let_defn : Format.formatter -> let_defn -> unit
-val print_rec_defn : Format.formatter -> rec_defn -> unit

src/mlw/ity.mli

@@ -13,7 +13,7 @@ open Ident
 open Ty
 open Term
 
-(** {2 Individual types (first-order types w/o effects)} *)
+(** {2 Individual types (first-order types without effects)} *)
 
 type itysymbol = private {
   its_ts      : tysymbol;       (** pure "snapshot" type symbol *)
@@ -256,40 +256,55 @@ val create_xsymbol : preid -> ity -> xsymbol
 
 (** {2 Effects} *)
 
+exception IllegalAlias of region
+exception AssignPrivate of region
+exception StaleVariable of pvsymbol * region
+exception BadGhostWrite of pvsymbol * region
+exception DuplicateField of region * pvsymbol
+exception WriteImmutable of region * pvsymbol
+exception GhostDivergence
+
 type effect = private {
-  eff_writes : Spv.t Mreg.t;
-  eff_resets : Sreg.t Mreg.t;
-  eff_raises : Sexn.t;
-  eff_diverg : bool;
+  eff_reads  : Spv.t;         (* known variables *)
+  eff_writes : Spv.t Mreg.t;  (* modifications to specific fields *)
+  eff_covers : Sreg.t Mreg.t; (* confinement of regions to covers *)
+  eff_taints : Sreg.t;        (* ghost modifications *)
+  eff_raises : Sexn.t;        (* raised exceptions *)
+  eff_oneway : bool;          (* non-termination *)
+  eff_ghost  : bool;          (* ghost status *)
 }
 
 val eff_empty : effect
-val eff_equal : effect -> effect -> bool
-val eff_union : effect -> effect -> effect
 
-val eff_is_empty : effect -> bool
-val eff_is_pure  : effect -> bool
+val eff_equal : effect -> effect -> bool
+val eff_pure : effect -> bool
 
-exception AssignPrivate of region
-exception DuplicateField of region * pvsymbol
-exception WriteImmutable of region * pvsymbol
+val eff_read : Spv.t -> effect
+val eff_write : Spv.t -> Spv.t Mreg.t -> effect (* drops writes outside reads *)
+val eff_assign : (pvsymbol * pvsymbol * pvsymbol) list -> effect (* r,field,v *)
 
-val eff_write : effect -> region -> Spv.t -> effect
-val eff_raise : effect -> xsymbol -> effect
-val eff_catch : effect -> xsymbol -> effect
-val eff_reset : effect -> region -> effect
+val eff_read_pre  : Spv.t -> effect -> effect (* no stale-variable check *)
+val eff_read_post : effect -> Spv.t -> effect (* checks for stale variables *)
+val eff_bind      : Spv.t -> effect -> effect (* removes variables from reads *)
 
-val eff_diverge : effect -> effect
+val eff_read_single      : pvsymbol -> effect
+val eff_read_single_pre  : pvsymbol -> effect -> effect
+val eff_read_single_post : effect -> pvsymbol -> effect
+val eff_bind_single      : pvsymbol -> effect -> effect
 
-val eff_assign : effect -> (region * pvsymbol * ity) list -> effect
+val eff_reset : effect -> region -> effect  (* confine to an empty cover *)
+val eff_strong : effect -> effect (* confine all subregions under writes *)
 
-val refresh_of_effect : effect -> effect
+val eff_raise : effect -> xsymbol -> effect
+val eff_catch : effect -> xsymbol -> effect
 
-exception IllegalAlias of region
+val eff_diverge : effect -> effect            (* forbidden if ghost *)
+val eff_ghostify : bool -> effect -> effect   (* forbidden if diverges *)
 
-val eff_full_inst : ity_subst -> effect -> effect
+val eff_contagious : effect -> bool           (* ghost and raising exceptions *)
 
-val eff_stale_region : effect -> ity -> bool
+val eff_union_seq : effect -> effect -> effect  (* checks for stale variables *)
+val eff_union_par : effect -> effect -> effect  (* no stale-variable check *)
 
 (** {2 Computation types (higher-order types with effects)} *)
 
@@ -304,57 +319,52 @@ type cty = private {
   cty_pre    : pre list;
   cty_post   : post list;
   cty_xpost  : post list Mexn.t;
-  cty_reads  : Spv.t;
   cty_effect : effect;
   cty_result : ity;
   cty_freeze : ity_subst;
 }
 
 val create_cty : pvsymbol list ->
-  pre list -> post list -> post list Mexn.t -> Spv.t -> effect -> ity -> cty
-(** [create_cty args pre post xpost reads effect result] creates a cty.
+  pre list -> post list -> post list Mexn.t -> effect -> ity -> cty
+(** [create_cty args pre post xpost effect result] creates a cty.
     The [cty_xpost] field does not have to cover all raised exceptions.
-    The [cty_reads] field contains all unbound variables from the spec.
-    The [cty_freeze] field freezes every pvsymbol in [cty_reads].
-    The [cty_effect] field is filtered wrt [cty_reads] and [args].
+    [cty_effect.eff_reads] is completed wrt the specification and [args].
+    [cty_freeze] freezes every unbound pvsymbol in [cty_effect.eff_reads].
+    All effects on regions outside [cty_effect.eff_reads] are removed.
     Fresh regions in [result] are reset. Every type variable in [pre],
     [post], and [xpost] must come from [cty_reads], [args] or [result]. *)
 
-val cty_apply :
-  ?ghost:bool -> cty -> pvsymbol list -> ity list -> ity -> bool * cty
-(** [cty_apply ?(ghost=false) cty pvl rest res] instantiates [cty]
-    up to the types in [pvl], [rest] and [res], then applies it to
-    the arguments in [pvl], and returns the ghost status and the
-    computation type of the result, [rest -> res], with every type
-    variable and region in [pvl] freezed. Typecasts into a mapping
-    type are allowed for total effectless computations. *)
+val cty_apply : cty -> pvsymbol list -> ity list -> ity -> cty
+(** [cty_apply cty pvl rest res] instantiates [cty] up to the types in
+    [pvl], [rest] and [res], then applies it to the arguments in [pvl],
+    and returns the computation type of the result, [rest -> res],
+    with every type variable and region in [pvl] being frozen. *)
+
+val cty_ghost : cty -> bool
+(** [cty_ghost cty] returns [cty.cty_effect.eff_ghost] *)
 
-val cty_r_visible : cty -> Sreg.t
-(** [cty_r_visible cty] returns the set of regions which are visible
-    from the non-ghost read dependencies and arguments of [cty]. *)
+val cty_ghostify : bool -> cty -> cty
+(** [cty_ghostify ghost cty] ghostifies the effect of [cty]. *)
 
-val cty_ghost_writes : bool -> cty -> Spv.t Mreg.t
-(** [cty_ghost_writes ghost cty] returns the subset of the write effect
-    of [cty] which corresponds to ghost writes into visible fields of
-    the ghost read dependencies and arguments of [cty]. *)
+val cty_reads : cty -> Spv.t
+(** [cty_reads cty] returns the set of external dependencies of [cty]. *)
 
 val cty_add_reads : cty -> Spv.t -> cty
-(** [cty_add_reads cty pvs] adds variables in [pvs] to [cty.cty_reads].
-    This function performs capture: if some variables in [pvs] occur in
-    [cty.cty_args], they are removed from [pvs], and the corresponding
-    type variables and regions are not frozen. *)
+(** [cty_add_reads cty pvs] adds [pvs] to [cty.cty_effect.eff_reads].
+    This function performs capture: if some variables in [pvs] occur
+    in [cty.cty_args], they are not frozen. *)
 
-val cty_add_pre : cty -> pre list -> cty
-(** [cty_add_pre cty fl] appends pre-conditions in [fl] to [cty.cty_pre].
+val cty_add_pre : pre list -> cty -> cty
+(** [cty_add_pre fl cty] appends pre-conditions in [fl] to [cty.cty_pre].
     This function performs capture: the formulas in [fl] may refer to
     the variables in [cty.cty_args]. Only the new external dependencies
-    in [fl] are added to [cty.cty_reads] and frozen. *)
+    in [fl] are added to [cty.cty_effect.eff_reads] and frozen. *)
 
 val cty_add_post : cty -> post list -> cty
 (** [cty_add_post cty fl] appends post-conditions in [fl] to [cty.cty_post].
     This function performs capture: the formulas in [fl] may refer to the
     variables in [cty.cty_args]. Only the new external dependencies in [fl]
-    are added to [cty.cty_reads] and frozen. *)
+    are added to [cty.cty_effect.eff_reads] and frozen. *)
 
 (** {2 Pretty-printing} *)
 
@@ -371,5 +381,6 @@ val print_pv   : Format.formatter -> pvsymbol -> unit (* program variable *)
 val print_pvty : Format.formatter -> pvsymbol -> unit (* pvsymbol : type *)
 val print_cty  : Format.formatter -> cty -> unit      (* computation type *)
 
-val print_spec : pvsymbol list -> pre list -> post list -> post list Mexn.t ->
-  Spv.t -> effect -> Format.formatter -> ity option -> unit (* piecemeal cty *)
+val print_spec :
+  pvsymbol list -> pre list -> post list -> post list Mexn.t ->
+    effect -> Format.formatter -> ity option -> unit (* piecemeal cty *)

src/parser/parser.mly

@@ -762,6 +762,12 @@ expr_sub:
     { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
 | expr_arg LEFTSQ expr LARROW expr RIGHTSQ
     { Eidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
+| expr_arg LEFTSQ expr DOTDOT expr RIGHTSQ
+    { Eidapp (sub_op $startpos($2) $endpos($2), [$1;$3;$5]) }
+| expr_arg LEFTSQ expr DOTDOT RIGHTSQ
+    { Eidapp (above_op $startpos($2) $endpos($2), [$1;$3]) }
+| expr_arg LEFTSQ DOTDOT expr RIGHTSQ
+    { Eidapp (below_op $startpos($2) $endpos($2), [$1;$4]) }
 
 loop_annotation:
 | (* epsilon *)

src/printer/smtv2.ml

@@ -57,7 +57,8 @@ let ident_printer =
       "concat"; "bvnot"; "bvand"; "bvor"; "bvneg"; "bvadd"; "bvmul"; "bvudiv";
       "bvurem"; "bvshl"; "bvlshr"; "bvult"; "bvnand"; "bvnor"; "bvxor";
       "bvcomp"; "bvsub"; "bvsdiv"; "bvsrem"; "bvsmod"; "bvashr"; "bvule";
-      "bvugt"; "bvuge"; "bvslt"; "bvsle"; "bvsgt"; "bvsge"; "rotate_left"; "rotate_right";
+      "bvugt"; "bvuge"; "bvslt"; "bvsle"; "bvsgt"; "bvsge"; "rotate_left";
+      "rotate_right";
 
       "cos"; "sin"; "tan"; "atan"; "pi";
 
@@ -129,12 +130,10 @@ let print_var_list info fmt vsl =
 let model_label = Ident.create_label "model"
 
 let collect_model_ls info ls =
-  if ls.ls_args = [] &&
-    Slab.mem model_label ls.ls_name.id_label then 
-    begin
-      let t = t_app ls [] ls.ls_value in
-      info.info_model <- (t_label ?loc:ls.ls_name.id_loc ls.ls_name.id_label t) :: info.info_model
-    end
+  if ls.ls_args = [] && Slab.mem model_label ls.ls_name.id_label then
+    let t = t_app ls [] ls.ls_value in
+    info.info_model <-
+      (t_label ?loc:ls.ls_name.id_loc ls.ls_name.id_label t) :: info.info_model
 
 (** expr *)
 let rec print_term info fmt t = 
@@ -320,15 +319,16 @@ let print_param_decl info fmt ls =
     (print_type_value info) ls.ls_value
 
 let print_logic_decl info fmt (ls,def) =
-  if Mid.mem ls.ls_name info.info_syn then () else
-  collect_model_ls info ls;
-  let vsl,expr = Decl.open_ls_defn def in
-  fprintf fmt "@[<hov 2>(define-fun %a (%a) %a %a)@]@\n@\n"
-    print_ident ls.ls_name
-    (print_var_list info) vsl
-    (print_type_value info) ls.ls_value
-    (print_expr info) expr;
-  List.iter forget_var vsl
+  if Mid.mem ls.ls_name info.info_syn then () else begin
+    collect_model_ls info ls;
+    let vsl,expr = Decl.open_ls_defn def in
+    fprintf fmt "@[<hov 2>(define-fun %a (%a) %a %a)@]@\n@\n"
+      print_ident ls.ls_name
+      (print_var_list info) vsl
+      (print_type_value info) ls.ls_value
+      (print_expr info) expr;
+    List.iter forget_var vsl
+  end
 
 let print_prop_decl args info fmt k pr f = match k with
   | Paxiom ->

src/session/session.ml

@@ -1173,6 +1173,7 @@ let load_result r =
             | "outofmemory" -> Call_provers.OutOfMemory
             | "failure" -> Call_provers.Failure ""
             | "highfailure" -> Call_provers.HighFailure
+            | "stepslimitexceeded" -> Call_provers.StepsLimitExceeded
             | s ->
                 Warning.emit
                   "[Warning] Session.load_result: unexpected status '%s'@." s;

theories/seq.why

@@ -165,5 +165,8 @@ end
   - UNPLEASANT: we cannot write s[1..] because 1. is recognized as a float
     so we have to write s[1 ..]
 
+  - UNPLEASANT: when using both arrays and sequences, the lack of overloading
+    is a pain; see for instance vstte12_ring_buffer.mlw
+
 *)