Arif reported it. https://github.com/dreal/dreal3/blob/master/src/tests/drh/arif.drh ```bash dReach -k 1 arif.drh ``` It gives us an immediate unsat result because the generated `.smt2` file includes the following: ```lisp (= mode_1 2) (= mode_1 4) ```