regression tests: use relative -solver_path to mathsat

[fbrausse]

This affects tests 172, 173, 182, 197 and fixes one issue observed in #61.

[zurabksmlp]

The old full path to mathsat should be removed but currently no path is added instead, and mathsat cannot be called. Is it assumed that a relative path like ../../../external/ will be used instead of an absolute path, or some MATHSAT_PATH variable will be introduced?

[fbrausse]

The old full path to mathsat should be removed but currently no path is added instead, and mathsat cannot be called. Is it assumed that a relative path like ../../../external/ will be used instead of an absolute path, or some MATHSAT_PATH variable will be introduced?

Indeed, using an environment variable for external tools either in general (like SMLP_SOLVER_PATH or so) or for each solver separately is a good idea, I think. I've setup my repo here s.t. ../../../external/ exists with MathSAT inside it. For the release I just wanted to get rid of the old Intel path structure to keep the regression tests consistent.

[fbrausse]

An alternative to introducing yet another environment variable would be setting the standard PATH and removing the mathsat-5.6.8-linux-x86_64-reentrant/bin/ component from the regression tests as well, only leaving -solver_path mathsat. That might be the cleanest approach, what do you think?

[zurabksmlp]

I think specifying a path explicitly in the command line would be best for clarity and also for debugging which version of mathsat is used or why it is not accessible. Since in regression we will have some directory structure regression script can use relative path, in other use cases a relative or absolute path can be used. A drawback could be that user should be aware of mathsat location, but in this specific case it should be OK since mathsat license is not as liberal as Z3 license and likely mathsat will not be packaged together with SMLP releases. In any case we do not need a decision now and I will approve the PR.

[zurabksmlp]

Approving this PR.

[zurabksmlp]

What I understand is that this change is for SMLP regression only. I think Dmitry has done similar changes in some of his PRs -- to remove Intel related paths from anywhere. Mathsat was located in the repo/external directory, and the regression script used absolute path rather than using relative path ../../external from repo/smlp/regr_smlp/code directory. <https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail> Virus-free.www.avast.com <https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail> <#DAB4FAD8-2DD7-40BB-A1B8-4E2AA1F9FDF2>

…

On Sat, Mar 21, 2026 at 4:22 PM Dmitry Messerman ***@***.***> wrote: *mdmitry1* left a comment (SMLP-Systems/smlp#63) <#63 (comment)> I don't understand this change solver-path is relative to some directory. Is this directory parallel to repository root directory? Another point - now this change significantly increases my effort, as I'll have to update automation scripts once again — Reply to this email directly, view it on GitHub <#63?email_source=notifications&email_token=BPWPDL4MMUPHWF644HWK5U34R2QRJA5CNFSNUABFM5UWIORPF5TWS5BNNB2WEL2JONZXKZKDN5WW2ZLOOQXTIMJQGM2DGNZRGIZKM4TFMFZW63VQOJSXM2LFO5PXEZLROVSXG5DFMSSWK5TFNZ2KYZTPN52GK4S7MNWGSY3L#issuecomment-4103437122>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/BPWPDL5BPMAELWRSZDQAOUL4R2QRJAVCNFSM6AAAAACWX2OKWCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHM2DCMBTGQZTOMJSGI> . You are receiving this because your review was requested.Message ID: ***@***.***>

[fbrausse]

Another point - now this change significantly increases my effort, as I'll
have to update automation scripts once again

@mdmitry1 Why do you think this change would affect anything you do at all?