Project

General

Profile

« Previous | Next » 

Revision ef609cc9

Added by Pierre-Loïc Garoche almost 4 years ago

Zustre: do not declare variables as Fixedpoint relations

View differences:

src/tools/zustre/zustre_common.ml
108 108
let decl_var id =
109 109
  Format.eprintf "Declaring var %s@." id.var_id;
110 110
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in
111
  Z3.Fixedpoint.register_relation !fp fdecl;
112 111
  register_fdecl id.var_id fdecl;
113 112
  fdecl
114 113

  

Also available in: Unified diff