Marco Eilers
Marco Eilers
I always use ``-Xss32m``, that's always been enough, but I won't give any guarantees ;)
This seems to have been fixed, the example now no longer leads to a Z3 error, but correctly reports a failing assertion.
Commit 01a41d8eae248fefb63933e21d59872fa40cfbe0 added a command line option ``--alternativeFunctionVerificationOrder`` which changes the computation of dependencies between functions to also take into account dependencies stemming from predicate unfoldings, which fixes the problem...
I'm wondering what the options are. - Is there an actual fix, can one set this to infinity or 1000000000, and if yes, would that be a good idea? -...
I'll check the timings with the changed value. For what it's worth, Silicon does use a non-default value for the other apparently-relevant parameter, ``(set-option :smt.qi.eager_threshold 100)`` I'm not really sure...
So this took forever, sorry, but here are the results. I ran the Silicon test suite, minus the graphs folder that contained examples that don't parse, three times, four repetions...
Great, thanks! I added the parameter commit 83ec94d2ee317991239ec4022461398e43b73da9.
Well, I don't know how that happened, but setting the lazy threshold to a high value *did* slow things down on the build server to the point that the build...
The underlying issue in Viper should be fixed (https://github.com/viperproject/silver/pull/649).
Silicon and Carbon both perform optimization of expressions, just not on the level of the input Viper program. Silicon does it on the level of its internal Terms, Carbon on...