mirror of
https://github.com/Z3Prover/z3
synced 2025-04-14 04:48:45 +00:00
add missing case handlers for internal bit-vector operators that leak during simplification
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
bbdcf2deaa
commit
f1d3a13b7f
|
@ -1073,6 +1073,12 @@ extern "C" {
|
|||
case OP_BSMUL_NO_OVFL:
|
||||
case OP_BUMUL_NO_OVFL:
|
||||
case OP_BSMUL_NO_UDFL:
|
||||
case OP_BSDIV_I:
|
||||
case OP_BUDIV_I:
|
||||
case OP_BSREM_I:
|
||||
case OP_BUREM_I:
|
||||
case OP_BSMOD_I:
|
||||
|
||||
return Z3_OP_UNINTERPRETED;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
|
|
Loading…
Reference in a new issue