smt

It's nice if testing doesn't produce unnecessary artifacts after running with success but keeps relevant info on fail for further inspection.

Pytest should have a nice way of creating fixtures that can post-process a test based on whether it failed or not https://docs.pytest.org/en/latest/example/simple.html#making-test-result-information-available-in-fixtures

If a test fails, then keep the

This is very low prio, but it usually happens that when touching Prims or some other file high in the dependency graph, we get spurious diffs in many other files. Since we check-in the snapshot, and we need to have it up-to-date, we get very verbose commits when nothing relevant changed. Plus, when something did change, it's hard to spot.

Example: I removed a few lines in prims and get things

At the moment, synthesis can take "hints" about auxiliary functions, which can be used for synthesing the main one. For instance, this is a specification for tree flattening that takes an auxiliary function:

{ lseg(x1, s1) ** lseg(x2, s2) ** ret :-> x2 }
void lseg_append (loc x1, loc ret)
{ s =i s1 ++ s2 ; lseg(y, s) ** ret :-> y }

{ z :-> x ** tree(x, s) }
void flatten(loc z)
{ z :

Currently, the SMT appends new side nodes to a slice at the end:

sideNodes = append(sideNodes, sideNode)
// ...
return reverseSideNodes(sideNodes)

This requires two allocations (one initially and one for the reverse slice) and one copy (to copy to the reverse slice). Alternatives