"...scala/leon/solvers/git@ic-gitlab.epfl.ch:lara/inox.git" did not exist on "1a0b9f9387fbbf48c39757c9bb2e2389b37597df"
Philippe Suter
authored
Without the flag, functions applied to ground arguments are treated the same way as every other one: by unrolling their body. This is suboptimal, as we can instead pass to Z3 the equality f(a0, a1) = v, instead of letting it "discover" it by itself. Note that this hasn't been shown to bring any major performance improvement; ground applications hardly show up in verification, for instance. But think about it, you'll agree using evaluation there is "The right thing to do.™". Note that testing --evalground currently highlights some bugs.
Name | Last commit | Last update |
---|---|---|
lib-bin | ||
library | ||
project | ||
regression | ||
src | ||
testcases | ||
unmanaged | ||
web | ||
.gitignore | ||
PERMISSIONS | ||
README | ||
build.sbt | ||
run-tests.sh |