Marco Gario
Marco Gario
The warning was a bit of a red herring. The problem was one we had already faced. The .so has a hardcoded value for the dylib that needs to be...
Instructions to test on an M1: ```sh # Clone the PR branch git clone --branch mathsat/5.6.7 [email protected]:pysmt/pysmt.git cd pysmt # Install Mathsat python3 install.py --msat --conf --force # ^ Should...
Thanks @chiara-camilla-rambaldi-migliore ! It seems we did fix the problem related to MathSAT, but there is a similar problem on the GMP dependency. ``` ld: warning: ignoring file /opt/homebrew/lib/libgmpxx.dylib, building...
:wave: @junichiro-kishi ! I agree with @mikand that this route might not be the best. The key problem I see is that psuedo-boolean is not part of the SMT-LIB. We...
No plans at the moment. I would be available to support an effort in this direction. The 2 time consuming parts of getting a new solver in are 1) understanding...
Thanks for the heads-up. If you feel like sharing the branch with your changes, it would be easier to judge how much work remains. > I needed algebraic types. I...
@mikand thanks for the patch in #588. I am overall ok with it, there are just a few suggestion on the PR. Overall, I think this is a bad idea...
Re-opening this, because I am not happy with the impact of supporting this. Do we have any evidence of a real use case in which this is useful?
The problem seems to occur only with python 3.5, and not python 2.7 . The segfault might also be due to memory limits on the instance that is running the...