Hi,
I have been experimenting with this library. However, during the experiments I realized that easy_smt is not able to extract negative solutions from the solver, e.g. integer types (i8, i16, ... ) .
Instead, if the solver return a negative solution, the library will just return the error NotAnAtom when trying to parse the solution to an unsigned integer type.
I looked a bit deeper into the code and created a draft PR here, which would add support for returning integer types.
Feel free to let me know what you think and whether there is some interest in this feature from your side.
Hi,
I have been experimenting with this library. However, during the experiments I realized that
easy_smtis not able to extract negative solutions from the solver, e.g. integer types (i8,i16, ... ) .Instead, if the solver return a negative solution, the library will just return the error
NotAnAtomwhen trying to parse the solution to an unsigned integer type.I looked a bit deeper into the code and created a draft PR here, which would add support for returning integer types.
Feel free to let me know what you think and whether there is some interest in this feature from your side.