Ahmed Irfan
Ahmed Irfan
fixes #318
> The tests fail. The one for CVC4 should be fixed once #529 is merged (seems to be related to an old SWIG version), but MathSAT seems unable to solve...
> The name of the test is very bad. There should be one test for a simple non linear expression and one for an irrational result. In the second case,...
Mathsat is failing on a test containing division by a variable.........
UPDATE: I extended the mathsat and cvc4 wrappers with the division operator. That should fix the division tests. Moreover, I simplified some NRA examples used in the test_solving.Basic. Regarding if...
@mikand or @marcogario : Could you please take a look why the tests for CVC4 are getting stuck? Thanks.
@mikand / @marcogario : tests are passing now on the new CI system. PR is ready for review....
@yuanyuan1024 Is this still an issue?
Reopen this if it is still an issue.
Also add a method called yices_model_set_term that maps a variable to the given term (term_t representing a value) -- as in yices_model_from_map