Michael Greenberg

That mostly makes sense... but I would expect `try` to be the process group in charge again after the inner shell exits. 🤔 Before we go down the rabbit hole...

We want: ``` # do the actual unshare, etc trap '' TTIN TTOU # prompt the user about committing ``` NB that I wrote `trap -` but meant `trap ''`....

> However, if the reading process is ignoring or blocking this signal, then read fails with an EIO error instead. ([GNU libc docs](https://www.gnu.org/software/libc/manual/html_node/Access-to-the-Terminal.html)) Well, joke's on me: that's not going...

Oh: `set -m` works because it will launch the user's command in a separate process group, which means they'll coordinate properly (and get the behavior I expected). We should `set...

The user can always run `try -- explore` if they have an `explore` command.

You can use the `bv` constructor---[symbolic evaluation has an example](https://github.com/HarvardPL/formulog/blob/a6138c91a5f1587a54a3c7f980f7726f1b8269b2/examples/symeval.flg#L66C1-L69C1). But per your second question, you'll be limited in how you work with such a bitvector: it's in SMT, so...

Right: you can't look at the "value" of a `bv[k] smt` without first getting a model---and then it's just the value in _that_ model. You're free to use such a...

Whoops, yes, I do, thank you!