dreal/dreal3

bug in dreach encoding

Opened this issue · 0 comments

soonho-tri commented

Arif reported it.
https://github.com/dreal/dreal3/blob/master/src/tests/drh/arif.drh

dReach -k 1 arif.drh

It gives us an immediate unsat result because the generated .smt2 file includes the following:

    (= mode_1 2)
    (= mode_1 4)