An early experiment.

• sbt test

• It works in Java v1.8. In Mac OS X: export JAVA_HOME=$(/usr/libexec/java_home -v1.8)

see HACKING.md

The rewrite method of GraphBuilderOpt in the LMS Backend has the "smart constructor" optimizations that, for example, optimizes read after write for arrays and variables.

The GraphBuilderOpt is linked through the Adapter object in the LMS Frontend. Because the linking is through an object as opposed to a trait, it's not easy to change -- so for now, we will experiment with more optimizations by changing LMS Clean directly.

• cd src/out
• cbmc --compact-trace interpcc_2sct_alt.check.c
• cbmc -DCBMC --refine --compact-trace --beautify --unwind 200 proci1b_staged_mul.actual.c