Marco Gario

Depending on what you mean by portfolio, this might be fairly simple. If by portfolio you mean "run solvers in parallel and get the first answer", you can do this...

Started work in https://github.com/pysmt/pysmt/pull/728

This is waiting for a new release of Yices that includes the fix.

Z3 Support added in PR #385. Look there to see what kind of changes might be involved.

The difference in messages in pysmt-install is due to thr fact that the python module is found but some othet issue exists. This us further shown by the exception that...

Is this ready for review?

:wave: Thanks for pushing this through! I will re-review this in the next few days. Since the PR description is almost 2yr old :older_man: , could you make sure that...

I did a first pass through all the issues and triaged them. There are [27 issues](https://github.com/orgs/pysmt/projects/1/views/1?groupedBy%5BcolumnId%5D=4736342&filterQuery=propose-closing%3A%22%F0%9F%94%A5+Yes%22 ) that I think we should just close as there is either not enough...

> Both SMTInterpol and OpenSMT 2 (master branch) can be used. Great! > I didn't also figure out how to better use named expressions (for the moment, named assertions are...

I am trying to upgrade to MathSAT 5.6.7 ( See [PR](https://github.com/pysmt/pysmt/pull/719) ). The [build fails ](https://github.com/pysmt/pysmt/runs/6637777176?check_suite_focus=true) with: ``` 80 warnings generated. creating build/lib.macosx-10.15-x86_64-3.8 g++ -bundle -undefined dynamic_lookup -L/usr/local/opt/sqlite/lib -L/usr/local/opt/sqlite/lib build/temp.macosx-10.15-x86_64-3.8/mathsat_python_wrap.o...