mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 05:18:44 +00:00
parent
73662ad60d
commit
eb205a5a40
|
@ -201,6 +201,7 @@ struct goal2nlsat::imp {
|
|||
case OP_XOR:
|
||||
case OP_NOT:
|
||||
case OP_IMPLIES:
|
||||
case OP_ITE:
|
||||
throw tactic_exception("convert goal into cnf before applying nlsat");
|
||||
case OP_DISTINCT:
|
||||
throw tactic_exception("eliminate distinct operator (use tactic '(using-params simplify :blast-distinct true)') before applying nlsat");
|
||||
|
|
Loading…
Reference in a new issue