Marco Gario

:wave: @h3xstream We have few additional expectations from the SARIF file that are stricter than what the standard requires. These are meant to provide a reasonable UI experience. One of...

Tests still seem to be failing, maybe this has to do with the upgrade of z3?

Do you think the segfault is related to the empty symbol? If so, I would not merge this feature as is. I think we have a very poor argument to...

The following snippet shows the support for Unsat Core. ``` python def demo_ucore_cvc4(): x = Symbol("x") with Solver(name="cvc4", solver_options={'produce-unsat-cores': "true"}) as s: s.add_assertion(x) s.add_assertion(Not(x)) r = s.solve() self.assertFalse(r) core =...

I agree, but this is a quite wide topic. From more of a "hands-on" overview, you can probably use some of the materials from prevoius SAT/SMT schools, e.g., [1]. From...

Next Step: Update README with the links from above.

Branch issue_187_enum_support, starts dealing with this issue. It currently only introduces the Enum Type at the Formula level. No translation to solver is performed (yet). https://github.com/pysmt/pysmt/tree/issue_187_enum_support

That was a quite old activity. I can try to find if I have a copy on my laptop. In between we changed how we handle types, so that would...

Ok, if this is the case, the I would suggest that we look into this in terms of supporting smtlib 2.6, meaning that we follow a design that is consistent...

The old branch is available as https://github.com/pysmt/pysmt/tree/i187/enum_support . As mentioned, I would probably look into adding the support for datatypes directly.