[enhancement][DSLX][formal] When proving quickchecks, assertions should become part of the proof objective

### What's hard to do? (limit 100 words)

Right now we don't convert assertions so you have to comment them out to run `prove_quickcheck_main` on your function of interest:

```
[ FAILED ] quickcheck_my_stuff: internal error: UNIMPLEMENTED: Unhandled node for conversion from XLS IR to Z3: assert_61057__1: token = assert(after_all.1134, nand.90861, message="Assertion failure via assert! @ foo.x:41:16-41:83", label="my_label", id=91275, pos=[(3,189,29)])
```

Ideally the assertion would become part of the quickcheck proof. Or maybe we could have a flag to say /whether/ the assertions should be proven as well, in case they make proving the quickcheck a lot less tractable.

### Current best alternative workaround (limit 100 words)

Just commenting out the asserts (and then not knowing whether they hold for all values in the quickcheck input domain).

### Your view of the "best case XLS enhancement" (limit 100 words)

We have a flag on `prove_quickcheck_main` that says whether to prove assertions as well -- when it's on they become part of the proof objective (and counterexamples we'll want to be shown as "this input failed that assertion"); when it's off we presumably just discard the assertions without giving an error.