This project is read-only.
If you run the Z3 axiom profiler, and it turns out to be thinking frequently about an axiom involving SeqIndex and SeqAppend, then you probably need this tip. Use the directive {:dafnycc_conservative_seq_triggers} on the affected method, and it should fix this problem.

Last edited Oct 15, 2014 at 12:13 AM by howell, version 1


No comments yet.