A problem when running Nopol (org.smtlib.SolverProcess$ProverException)

[DehengYang]

I have configured Nopol in my PC with Ubuntu 14.04 ( including install cocospoon, JDK 1.7, etc.)

However, when I run Nopol to repair bugs (e.g. Chart_5, Chart_9, Lang_44), I find that Nopol cannot output an expected patch. The related info is as follow:

10:42:12.675 [pool-2-thread-1] ERROR fr.inria.lille.repair.nopol.NoPol - deheng Timeout: execution time > 30 SECONDS
java.util.concurrent.ExecutionException: org.smtlib.SolverProcess$ProverException: The solver has not been started
	at java.util.concurrent.FutureTask.report(FutureTask.java:122) [na:1.7.0_80]
	at java.util.concurrent.FutureTask.get(FutureTask.java:202) [na:1.7.0_80]
	at fr.inria.lille.repair.nopol.NoPol.executeNopolProcessor(NoPol.java:400) [nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at fr.inria.lille.repair.nopol.NoPol.runOnStatement(NoPol.java:375) [nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at fr.inria.lille.repair.nopol.NoPol.solveWithMultipleBuild(NoPol.java:289) [nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at fr.inria.lille.repair.nopol.NoPol.build(NoPol.java:149) [nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at fr.inria.lille.repair.Main$1.call(Main.java:93) [nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at java.util.concurrent.FutureTask.run(FutureTask.java:262) [na:1.7.0_80]
	at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1145) [na:1.7.0_80]
	at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:615) [na:1.7.0_80]
	at java.lang.Thread.run(Thread.java:745) [na:1.7.0_80]
Caused by: org.smtlib.SolverProcess$ProverException: The solver has not been started
	at org.smtlib.SolverProcess.send(SolverProcess.java:126) ~[nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at org.smtlib.SolverProcess.sendAndListen(SolverProcess.java:139) ~[nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at org.smtlib.solvers.Solver_z3_4_3.set_option(Solver_z3_4_3.java:386) ~[nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at org.smtlib.command.C_set_option.execute(C_set_option.java:71) ~[nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at org.smtlib.impl.Script.execute(Script.java:107) ~[nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at fr.inria.lille.commons.synthesis.smt.SMTLibScriptSolution.hasMoreElements(SMTLibScriptSolution.java:32) ~[nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at fr.inria.lille.commons.synthesis.smt.SMTLib.anySolutionFor(SMTLib.java:323) ~[nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at fr.inria.lille.commons.synthesis.ConstraintBasedSynthesis.scriptSolution(ConstraintBasedSynthesis.java:177) ~[nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at fr.inria.lille.commons.synthesis.ConstraintBasedSynthesis.satisfyingSolution(ConstraintBasedSynthesis.java:167) ~[nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at fr.inria.lille.commons.synthesis.ConstraintBasedSynthesis.codesSynthesisedFrom(ConstraintBasedSynthesis.java:72) ~[nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at fr.inria.lille.repair.nopol.synth.SMTNopolSynthesizer.buildPatch(SMTNopolSynthesizer.java:100) ~[nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at fr.inria.lille.repair.nopol.NoPol.runNopolProcessor(NoPol.java:429) [nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at fr.inria.lille.repair.nopol.NoPol.access$000(NoPol.java:67) [nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	at fr.inria.lille.repair.nopol.NoPol$1.call(NoPol.java:393) ~[nopol-0.2-SNAPSHOT-jar-with-dependencies.jar:na]
	... 4 common frames omitted

I think this is not a timeExecution exception... I have got no idea & solution about the failure.
Much appreciated if any help is provided!

[tdurieux]

I have this issue when the path the z3 is incorrect or when the z3 has been compiled for a different architecture.

Can you try in compile it from scratch: https://github.com/Z3Prover/z3
and give the valid path in the configuration?

[DehengYang]

Thank you so much for your help!

Sorry for my late feedback... Inspired by your suggestion, I replace the z3 in the Nopol configured in my PC with the z3 from the original Nopol folder (https://github.com/SpoonLabs/nopol/tree/master/nopol/lib/z3), then the Nopol works well.

Thank you again for your help!