search

stanford-centaur / smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.
Other
103 stars 40 forks source link

multiplication is variadic #341

Closed ffrohn closed 9 months ago

ffrohn commented 9 months ago

This allows for creating multiplication-terms with more than two arguments with Z3. Currently, such terms can be created with CVC5, but not with Z3 (I didn't try other solvers).

yoni206 commented 9 months ago

Thanks! Could you please include a test for this new feature? Perhaps the best place would be to add a test here? https://github.com/stanford-centaur/smt-switch/blob/master/tests/test-int.cpp

This would also clarify the status with the other solvers.