Andrew V. Teylu

> The static build currently disables the python interface, and the python interface is required for testing. So getting testing of the static working will require changes to the build...

It seems that this is because the `let` is introduces a term with a name that already exists: ``` (set-logic QF_BV) (declare-fun u () (_ BitVec 1)) (assert (let ((u...

Also doesn't work: ``` (set-logic QF_BV) (declare-fun u () (_ BitVec 1)) (assert (let ((v (_ bv0 1))) (let ((v (_ bv0 1))) (= (_ bv0 1) (_ bv0 1)))))...

A naive implementation gives `sat` on this when it shouldn't: ``` (set-logic QF_BV) (set-info :status unsat) (declare-fun u () (_ BitVec 5)) (assert (not (= (_ bv0 5) (let ((u...

As far as I’m aware, nope. SMTLIB allows lets to shadow other symbols (and lets shadowing lets) — STP’s let manager cannot handle this. At least, that’s my understanding for...

Basically, from my memory, symbols get resolved (by STP) “globally” first and then in the let manager. If a let shadows a global symbol, STP resolves it globally and ignores...

@conp-solutions you're not currently on the STP "team", which means, even if I create a branch on the main STP repo, you won't be able to push to it. The...

Hmm, I'm not sure that this is immediately mergeable. Basically, this no longer works: ```bash export PYTHONPATH=$(readlink -f bindings/python/stp) python3 ./bindings/python/stp/stp.py ``` This is then a problem if we have...

Don't get me wrong; people from _should_ point to one level above, but I am not sure they do.

Yeah, because our `__init__.py` imports from `.stp` ... not my code, but code that exists nonetheless!