Facundo Domínguez
Facundo Domínguez
I dived some more into the FFI path, and its looking laborious. smt-switch doesn't support parametric datatypes, apparently, and neither there is good documentation on the z3 bindings to define...
The result is unchanged when eliminating those qualifiers. These are the stats with no modifications ``` # Sub Constraints : 243 # WF Constraints : 102 # Constraints : 208...
Will the second parameter of the qualifier `x : e##xo` be substituted with values of any sort? This could perhaps explain a long list of qualifiers created by replacing `x`...
They originate from the specification of typeclass methods. ```Haskell class Lexicographic e where terminate :: e -> Int -> Bool size :: e -> Int index :: Int -> e...
> Oddly though those two qualifiers seem to come from somewhere else: as they respectively check if lexSize equals or is greater than 0? Aren't the comparisons made with `VV##0`...
Removing only the qualifiers with unrestricted parameters, gives ``` # Sub Constraints : 243 # WF Constraints : 102 # Constraints : 208 # Refine Iterations : 746 # SMT...
I don't follow that argument. Maybe an example is in order.
The example seems wrong. That `fail` call is not evaluated in the NC thread.
> would it be helpful to solicit help maintaining this package? Possibly. Note that the current maintainer is Tim Watson, though. Let me know if I can help setting up...
Tracing does show it. But I think @Shimuuar is asking for a heads up in `stderr` with no tracing enabled.