"src/main/scala/leon/git@ic-gitlab.epfl.ch:lara/inox.git" did not exist on "76e4a4a50af5d17a80a4ce64e24b4c4716570876"
Etienne Kneuss
authored
Assert may not be helping at all. It is trimming crucial information from the formula, i.e. [[ a,b ; a = size(x) AND a+1 = size(b); x ]]. Applying assert will remove 'a+1 = size(b)' from phi and push it as precondition when reconstructing a solution. The subproblem will become: [[ a,b ; a = size(x) ; x]] The input 'b' is then removed by applying Unused-Input.
Name | Last commit | Last update |
---|---|---|
lib-bin | ||
library | ||
project | ||
regression | ||
src | ||
testcases | ||
unmanaged | ||
.gitignore | ||
PERMISSIONS | ||
README | ||
TODO | ||
build.sbt | ||
run-tests.sh |