mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e33e66212c
commit
343603f643
|
@ -270,7 +270,7 @@ class bv_expr_inverter : public iexpr_inverter {
|
||||||
|
|
||||||
bool process_bv_mul(func_decl* f, unsigned num, expr* const* args, expr_ref& r) {
|
bool process_bv_mul(func_decl* f, unsigned num, expr* const* args, expr_ref& r) {
|
||||||
if (num == 0)
|
if (num == 0)
|
||||||
return nullptr;
|
return false;
|
||||||
if (uncnstr(num, args)) {
|
if (uncnstr(num, args)) {
|
||||||
sort* s = args[0]->get_sort();
|
sort* s = args[0]->get_sort();
|
||||||
mk_fresh_uncnstr_var_for(f, r);
|
mk_fresh_uncnstr_var_for(f, r);
|
||||||
|
|
Loading…
Reference in a new issue