DecisionProcedureTest fails due to hard-coded z3 path

[andreamattavelli]

Hard-coding paths is a bad solution, since the build will likely fail on different environments. A possible solution would be to rely on an environment variable, and then assumeTrue that the path exists. This has the effect that: if the environment variable is not set, the path will be null and the test skipped since the assumption does not hold.

A possible sketch of the solution:

@Before
public void setUp() throws DecisionException {
  String z3Path = System.getenv("z3_path");
  Assume.assumeTrue(z3Path!=null);
  this.dec =
     new DecisionProcedureAlgorithms(
        new DecisionProcedureSMTLIB2_AUFNIRA(new DecisionProcedureAlwSat(), this.calc, z3Path + " -smt2 -in -t:10"),
        this.calc);
}

Any better idea?

[pietrobraione]

I don't like very much the idea of making tests dependent on environment variables, especially if we want to keep everything IDE-friendly. Note that it's not really the build to fail, it's just that some tests do not pass (which, it's true, may stop the build at some point). I think that a way to improve the things could be let the test fail and report the issue by an error message pointing to the location in the test code where the developer can find the variable that should be changed.

[andreamattavelli]

@pietrobraione I actually don't understand your comment. Environment variables are IDE- and OS-independent, so why shouldn't they be IDE-friendly? Moreover, hard-coded paths are everything-unfriendly. A typical user wants to download a tool, compile it, check that is works (in her environment), and package it. Currently, this is not possible: mvn package fails due to the hard-coded path. So one needs to download, and modify unfamiliar code to make everything work. This is not a great solution. My proposal is more oriented on the Assume rather than the environment variable. Whatever solution you want to apply, on should not be forced to fix the path in the tests.