Closed soonhokong closed 2 years ago
We can handle QF_LIA, QF_LIRA, QF_NIA, and QF_NIRA. But dReal throws an exception when it detects those logic.
QF_LIA
QF_LIRA
QF_NIA
QF_NIRA
We can handle
QF_LIA
,QF_LIRA
,QF_NIA
, andQF_NIRA
. But dReal throws an exception when it detects those logic.