IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
77
stars
24
forks
source link
controlling incremental option for individual isolates #75
I am working a project using IVy and there are around 140 isolates. Each isolate checks ok individually but when I try to check the whole project at once, the Z3 calls get stuck for a long time mid way. I tried using the incremental=false option but this causes some of the isolates to get stuck for a long time that would pass easily with incremental=true. Is there a way to control the incremental option for individual isolates using attributes within the ivy models? Or is there a way to flush Z3 after each isolate?
I am working a project using IVy and there are around 140 isolates. Each isolate checks ok individually but when I try to check the whole project at once, the Z3 calls get stuck for a long time mid way. I tried using the incremental=false option but this causes some of the isolates to get stuck for a long time that would pass easily with incremental=true. Is there a way to control the incremental option for individual isolates using attributes within the ivy models? Or is there a way to flush Z3 after each isolate?