From b1239d52766318417c1b50d8f22f9f2fce8849c1 Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer Date: Thu, 5 Jan 2023 18:05:08 +0100 Subject: [PATCH] Missing file --- src/math/polysat/op_constraint.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp index 4e19c2d43..6f372c870 100644 --- a/src/math/polysat/op_constraint.cpp +++ b/src/math/polysat/op_constraint.cpp @@ -671,6 +671,9 @@ namespace polysat { case code::and_op: us.add_and(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep); break; + case code::inv_op: + us.add_inv(pv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep); + break; default: NOT_IMPLEMENTED_YET(); break;