Project

General

Profile

« Previous | Next » 

Revision 07ceae4c

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

[HORN] Protect names of stateless nodes with a _fun suffix. This was conflicting with existing names in Z3, ie. "abs".
[HORN] Better treatment of stateless nodes collecting semantics
Fixes issue #13 on github: https://github.com/coco-team/lustrec/issues/13

View differences:

src/backends/Horn/horn_backend_common.ml
16 16 

  		




  17
  17
  
    
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id


  		




  18
  18
  
    
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id


  		




  19
  
  
    
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id


  		




  
  19
  
    
let pp_machine_stateless_name fmt id = fprintf fmt "%s_fun" id


  		




  20
  20
  
    

  		




  21
  21
  
    
let rec pp_type fmt t =


  		




  22
  22
  
    
  match (Types.repr t).Types.tdesc with


  		












Also available in:  Unified diff