Project

General

Profile

« Previous | Next » 

Revision 8eeec77e

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

Filtering out ERR and MAIN from the forall quantification

View differences:

src/tools/zustre/zustre_analyze.ml
138 138
      ]
139 139
  in
140 140
  let _ =
141
    add_rule []  (Z3.Boolean.mk_implies !ctx horn_body horn_head)
141
    add_rule ~dont_touch:[decl_main] []  (Z3.Boolean.mk_implies !ctx horn_body horn_head)
142 142
      
143 143
  in
144 144

  
......
152 152
  let not_prop =
153 153
    Z3.Boolean.mk_not !ctx prop
154 154
  in
155
  add_rule main_memory_next (Z3.Boolean.mk_implies !ctx
155
  add_rule ~dont_touch:[decl_main;decl_err] main_memory_next (Z3.Boolean.mk_implies !ctx
156 156
	      (
157 157
		Z3.Boolean.mk_and !ctx
158 158
		  [not_prop;

Also available in: Unified diff