Andrew V. Teylu

z3 uses `(maximize )` and `(minimize )` for this (I think it comes *before* the `check-sat` call) -- so calling `check-sat` does the maximisation/minimisation. afaik, this isn't standard though (e.g.,...

I guess the idea about iteratively flipping bits (from `0` -> `1`) for the maximise case seems reasonable, but we'd need to handle the unsigned case (i.e., you don't want...

I might be able to take a look at `global-declarations` -- do you have a small, self-contained example of where this makes sense/is necessary? This is where the SMTLIB2 front-end...

If you care about `global-declarations`, do you also care about `reset-assertions`?

Baby-steps: if you can provide an easy/minimal/self-contained example, I can take look at getting that working (but no promises). Then, once the easy bit is done, we can take a...

If you don't have `global-declarations` and you `pop` a previous symbol, do you expect to able to have the ability to create a symbol with a different type? I would...

Okay, so that's what I expected (without reading it). Think about this: ``` (set-option :global-declarations false) (push 1) (declare-fun x!0 () Bool) (assert (not x!0)) (check-sat) (get-model) (pop 1) (push...

I’m happy to take a look/give it ago, and I should be able to take a look this week. That being said, I was offering more as way to learn...

Weirdly, this "works" (when we don't want it to): ``` (push 1) (declare-fun x!1 () Bool) (define-fun x!2 () Bool (not x!1)) (pop 1) (assert (not x!1)) ``` but this...

Ah! I think when you use `x!2` in a function declaration (like with `x!3`) then the reference count of `x!2` is _two_ (once for itself and once for its use...