mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
add checks in internalizer for issues of the form #227
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4fd1f4a65c
commit
fb624780d5
|
@ -617,8 +617,15 @@ namespace smt {
|
|||
mk_ite_cnstr(to_app(n));
|
||||
add_ite_rel_watches(to_app(n));
|
||||
break;
|
||||
case OP_TRUE:
|
||||
case OP_FALSE:
|
||||
break;
|
||||
case OP_DISTINCT:
|
||||
case OP_IMPLIES:
|
||||
case OP_XOR:
|
||||
UNREACHABLE();
|
||||
case OP_OEQ:
|
||||
case OP_INTERP:
|
||||
UNREACHABLE();
|
||||
default:
|
||||
break;
|
||||
|
|
Loading…
Reference in a new issue