Soonho Kong

FWIW, I have an intel mac where I can reproduce the same issue. My environment: - macOS 10.15.7 - cmake 3.19.2 I cloned this repo (sha `a670b786539d3c8865d8f68fe0c67a2d4afbf1aa`) and run `cmake`...

@kepler471 , thanks. I can confirm that using cmake 3.19.3 resolves this issue on my side (note: I'm not using an M1 mac).

We do not provide that functionality in Python API yet. To implement this functionality, one has to wrap [`Smt2Driver` class](https://github.com/dreal/dreal4/blob/master/dreal/smt2/driver.h) using [pybind11](https://github.com/pybind/pybind11). You can find some examples in https://github.com/dreal/dreal4/blob/master/dreal/dreal_py.cc.

This is because we process a `let_binding_list` and add the temporary terms (i.e. `L0\y = x + 1`) at the top-level. This strategy works for the `exist`-case but does not...

We need more than this since we also have `let`-expressions.

@benjholla , we do not have a specific timeline for this.

I guess the issue is that I didn't consider the case where we have Boolean variables inside of the universal quantifiers which we have in your example (via `if_then_else`). I'll...

BTW, ```python if_then_else(b == True, 1 , -1) ``` `b == True` doesn't sound correct given the fact `b : Int`.

There are two issues here: 1) If-then-else eliminator does not support `forall` formulas yet. https://github.com/dreal/dreal4/blob/5e7c80ab49ac976718da020acc959480640a31d7/dreal/util/if_then_else_eliminator.cc#L336-L357 2) There is an ambiguity in `formula == formula` (i.e. `iff`) and `expr == expr`...

Hi @rohit507 , as Sean mentioned we only support one alternation of quantifiers (exists-forall). If you mean nested "universal" quantifiers, then it's easy to collapse them into a single quantifier...