Skip to content

Quick'n'dirty fix for SimplifierWithPC

Viktor Kuncak requested to merge simplifier into master

Created by: mantognini

This ensures that the trait is thread safe. This is required for the concurrency introduced by epfl-lara/stainless#76.

Ideally, it's internal state shouldn't be mutable and/or the critical section should be reduced to its minimal size for better throughput efficiency.

I couldn't provide a more efficient patch mainly because this feature is not well documented and I couldn't infer all the assumptions easily. This is therefore more a temporary workaround than a proper patch. I basically added synchronized on all publicly available methods' body.

Merge request reports