Ahmed Irfan

Results 16 comments of Ahmed Irfan

> 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....

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