Solver processes leak or deadlock #77

Medium. Incremental solver processes are never terminated (one leaked solver per synthesis, and Synthesizer.__exit__ is not a working context manager); solver output is not drained between check-sats, so SMTInterpol deadlocks on 4-qubit instances; and the bundled SMTInterpol wrapper writes error.log into the caller's directory and hides failures.

Found in a code review of master at 66b41d9. Every item below was reproduced; the IDs (F1, G2, ...) are the review's.

Items: F35, F36, F72

F35

Incremental SMT solver processes are never terminated (one leaked solver per synthesis), and Synthesizer.exit is not a working context manager

Location: src/solvers.py:63 · severity: medium

SMTSolver.create_process starts the persistent solver (stdin/stdout/stderr pipes, no start_new_session), and nothing ever closes stdin, kills or reaps it: not on success, not at max_depth, not on exceptions. synthesis() only calls exit() for pysmt. Synthesizer.exit(self) (synth.py:79) has the wrong signature and there is no enter, so with Synthesizer() raises TypeError. In long-running processes (tests, benchmark loops, notebooks) solvers pile up; a solver killed mid-check keeps running as an orphan until the check ends; the undrained stderr pipe can also block a chatty solver (see F36).

Reproduction. Three consecutive Synthesizer().synthesis(..., solving='smt', solver='yices2', mode='incremental') calls leave three live yices_smt2 children. A yices_smt2 --incremental orphan (PPID 1) running for nearly 3 hours was present on the review machine.

runtime leak.py: after three synthesis() calls and gc.collect(): 3 x '/home/ondra/milq/solvers/yices2/yices_smt2 --incremental'.
quality leak.py: live child solver processes after run 1/2/3: 1, 2, 3. differential leak.py: same; `ps -p 3546420` -> ppid 1, etime 02:58:47, yices_smt2 --incremental.

Suggested fix. Add SMTSolver.close(): send (exit), close stdin, wait with a timeout, then kill the process group (start it with start_new_session=True as the portfolio does). Call it from a try/finally in synthesis() for every solving mode. Replace exit with a proper enter/exit(self, exc_type, exc, tb) pair or a close() method.

F36

The incremental protocol never drains solver output between check-sats; SMTInterpol (print-success) deadlocks on 4-qubit instances

Location: src/solvers.py:76 · severity: medium

In incremental mode stdout is read only after (check-sat) (solve) or (get-value) (get_model), and stderr is never read. SMTInterpol prints 'success' after every command (the comment at solvers.py:77 confirms it; the wrapper does not pass -no-success). After about 8,192 unread 'success' lines (64 KiB pipe) the solver blocks on write and stops reading stdin, and MILQ's next write_incremental blocks on the full stdin pipe: a silent deadlock with no CPU use and no timeout. The same happens if any solver writes > 64 KiB to stderr, or prints many (error ...) lines, between two check-sats.

Reproduction. milq -s smt -a smtinterpol benchmarks/ghz/4.qasm (default -m incremental, -v all) sends 22,425 statements before the first (check-sat) and hangs forever during encoding.

deadlock.py (incremental SMTSolver + fake_solver 'success+sat', N asserts then check-sat): N=5000 -> 'answer: sat 0.0s'; N=40000 -> 'written 0 / written 5000 / written 10000' then hangs, exit 124 (timeout 20).
count4.py (yices2): benchmarks/ghz/4.qasm -v all sends 22425 statements before the first check-sat. Jar usage: '-no-success  Don't print success messages.' (Java not installed here; real SMTInterpol not run.)

Suggested fix. Send '(set-option :print-success false)' first in Generator.set_incremental_mode, or add -no-success to SMTInterpol's flags. More robustly, read stdout and stderr in background threads into a queue so writes never depend on the reader; solve/get_model consume from the queue (with an optional timeout).

F72

Bundled SMTInterpol wrapper writes error.log into the caller's directory, hides failure messages, and enables SMT-COMP self-checking

Location: solvers/smtinterpol/smtinterpol:4 · severity: low

The SMT-COMP run script ends with 2>error.log, relative to the current directory, so every SMTInterpol start (including every portfolio solve, since smtinterpol is a portfolio member) creates or overwrites error.log in the user's working directory. _describe_failure then sees empty stderr and reports 'no output' even when the cause is in that file (e.g. 'java: command not found'). The script also enables -o proof-check-mode -o model-check-mode (overhead not measured without Java) and leaves $SCRIPTDIR unquoted. PR #55's solvers.toml still points at this wrapper.

Reproduction. A user without Java runs -a smtinterpol (or -a portfolio) and gets 'smtinterpol failed, exit code 127 (command not found): no output' plus an unexplained error.log in the project directory.

$ milq two.qasm -s smt -a smtinterpol -> 'synthesis failed: smtinterpol failed, exit code 127 (command not found): no output'; cat ./error.log -> 'line 4: java: command not found'. quality out_port listing after -a portfolio: error.log out.qasm out.smt2 synth.log.

Suggested fix. Use a MILQ-specific wrapper: exec java -jar "$SCRIPTDIR/smtinterpol.jar" -no-success "$@", leaving stderr on the pipe MILQ already captures, and drop the proof/model-check modes.