bug fix: solver cannot eval on python 3.11

In newer versions of python, the C API
is more strict, and will not attempt to type-coerce,
instead preferring to raise an exception.

This change passes the yices ID explicitly to
`get_value_as_term` -- I believe that in lower versions,
it was coercing the `YicesTerm` to a string
via __str__, then coercing that to an int,
and which happens to be its ID.

greed/solver/yices2.py

@@ -449,13 +449,13 @@ def Array_Select(self, arr: YicesTermArray, index: YicesTermBV) -> YicesTermBV:
         yices_id = yices.Terms.application(arr.id, [index.id])
         return YicesTermBV(operator="select", children=[arr, index], yices_id=yices_id)
 
-    def eval(self, term, raw=False):
+    def eval(self, term: YicesTerm, raw=False):
         assert self.is_sat(), "Formula is UNSAT"
         model = yices.Model.from_context(self.solver, 1)
         if raw:
-            return YicesTermBV(model.get_value_as_term(term))
+            return YicesTermBV(model.get_value_as_term(term.id))
         else:
-            return self.bv_unsigned_value(YicesTermBV(model.get_value_as_term(term)))
+            return self.bv_unsigned_value(YicesTermBV(model.get_value_as_term(term.id)))
 
     def copy(self):
         new_solver = Yices2()