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 14, 2014 at 11:13 PM by howell, version 1

Comments

No comments yet.