diff --git a/src/math/polysat/smul_fl_constraint.cpp b/src/math/polysat/smul_fl_constraint.cpp index cd6e20aec..c529479e2 100644 --- a/src/math/polysat/smul_fl_constraint.cpp +++ b/src/math/polysat/smul_fl_constraint.cpp @@ -126,5 +126,7 @@ namespace polysat { us.add_smul_ovfl(p_coeff, q_coeff, !is_positive, dep); else us.add_smul_udfl(p_coeff, q_coeff, !is_positive, dep); + return mk_mix(p().hash(), q().hash(), kind()); } + }