Project

General

Profile

« Previous | Next » 

Revision 8c934ccd

Added by Pierre-Loïc Garoche about 3 years ago

lustrev seal: ongoing work on extraction as dynamical system. Still not working yet

View differences:

src/tools/zustre/zustre_test.ml
213 213 

  		




  214
  214
  
    
  let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in


  		




  215
  215
  
    

  		




  216
  
  
    
  Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status)


  		




  
  216
  
    
  Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);


  		




  
  217
  
    

  		




  
  218
  
    

  		




  
  219
  
    
  let ts = Z3.Tactic.get_tactic_names !ctx in


  		




  
  220
  
    
  List.iter (fun s -> Format.printf "%s@." s) ts;


  		




  
  221
  
    
  ()


  		




  217
  222
  
    
    


  		




  218
  223
  
    
	


  		




  219
  224
  
    

  		












Also available in:  Unified diff