Merge the folk work to hint-learning branch

ChenchengLiang commented 4 years ago

Merge to hint-learning branch

pruemmer commented 4 years ago

Thanks for the pr; I'm getting a build error however, can you add a correct reference to this library?

[info] Resolving play#play_2.10;2.1.0 ... [warn] module not found: play#play_2.10;2.1.0 [warn] ==== local: tried [warn] /home/philipp/.ivy2/local/play/play_2.10/2.1.0/ivys/ivy.xml [warn] ==== public: tried [warn] https://repo1.maven.org/maven2/play/play_2.10/2.1.0/play_2.10-2.1.0.pom [warn] ==== uuverifiers: tried [warn] http://logicrunch.research.it.uu.se/maven/play/play_2.10/2.1.0/play_2.10-2.1.0.pom

ChenchengLiang commented 4 years ago

Thanks for the pr; I'm getting a build error however, can you add a correct reference to this library?

[info] Resolving play#play_2.10;2.1.0 ... [warn] module not found: play#play_2.10;2.1.0 [warn] ==== local: tried [warn] /home/philipp/.ivy2/local/play/play_2.10/2.1.0/ivys/ivy.xml [warn] ==== public: tried [warn] https://repo1.maven.org/maven2/play/play_2.10/2.1.0/play_2.10-2.1.0.pom [warn] ==== uuverifiers: tried [warn] http://logicrunch.research.it.uu.se/maven/play/play_2.10/2.1.0/play_2.10-2.1.0.pom

Yes. I modified build.sbt again in commitment 71f8c8e. It will now build correctly.

ChenchengLiang commented 4 years ago

Thanks for pointing out them. New commits fixed these problems.

pruemmer commented 4 years ago

Thanks! I'm afraid I have some more comments:

Could you make the class StaticAbstractionBuilderSmtHintsSelection a subclass of StaticAbstractionBuilder?
Add your name in the preamble of files you added/changed
Make sure that the regression tests pass. At the moment all seem to fail because your branch produces some debugging output by default. Such output should only happen when the right option is given?

uuverifiers / eldarica