Thomas Sewell

After discussion with colleagues, we note that Z3 4.12 does seem to solve the most challenging of these (mut_tree_z3.smt2.txt) whereas previous Z3 versions seemed to time out on it entirely....

Thanks for that hint. It does indeed seem to solve the performance problem, when processing this problem as a standalone instance. It doesn't seem to make much difference when using...

We've continued with this, have a new example, and some more questions. We now have a smaller example that clearly demonstrates the timeout. This example is, essentially, a simple identity...

OK, I'll add a bit more of my thinking. The dependency information is already cached in the `.d` files, but only for "built in" build commands. There doesn't seem to...

Sorry, I think I'd misunderstood some of your points. I didn't realise `Holmake` used an alternative startup process. To clarify, the problem I see is on the `Holmake` side. Interactive...

To follow up, I'm happy to leave this for the moment and spend some cycles thinking about what we're aiming for here. I guess my claim was that loading of...

I can be more specific. Many parts of the translator and characteristic Lib code make use of EVAL in particular to do ... all kinds of things. There are a...

Also, while working on the nsLookup changes (issue #527 ) I struggled with this a lot, until I figured out how to add my new code as a conv to...

Hmm, sorry, no. Putting this issue up was a (not very effective) way of documenting a deficiency of the system. I didn't end up with any cycles to work on...

Does anyone remember what was the issue here? EVAL requires a safe way to write code then execute it. At the moment that's done by setting the EVAL code buffer...