Alex Light

NB That the IR already supports verbosity levels in trace_fmt! but this isn't exposed to DSLX. Having support for this would be nice.

Splitting this into DSLX type things and proc-jit-wrapper https://github.com/google/xls/issues/1402 and jit-wrapper improvements https://github.com/google/xls/issues/1403.

So it seems like it would be somewhat helpful to get some more details about what exactly you think a good result would be. Reading this and your other bugs...

As far as we can tell our smtlib emitter fully supports [umod](https://github.com/google/xls/blob/6958511f4fe69e7b364e726666f8b6d79eb6161c/xls/solvers/z3_ir_translator.cc#L377) and [smod](https://github.com/google/xls/blob/6958511f4fe69e7b364e726666f8b6d79eb6161c/xls/solvers/z3_ir_translator.cc#L446). Manual tests indicate this all works: ``` allight@wenix ‹ main › : ~/xls [0] % cat...

You need to update your xls build to a more recent one. That error message is from the z3_ir_translator.cc and at some point between that 2 year old commit and...

It seems to be working fine for me. Possibly it was down temporarily. If its still not working I'm not sure we can really help you very much since it...