From 25b5b985e6f025e5467ea6376410d9e8f32c5359 Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
Date: Wed, 7 Sep 2022 18:02:06 +0200
Subject: [PATCH] Missing overload for conflict (#6329)

---
 src/api/c++/z3++.h | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 8d3a70b8b..0275a22e1 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -4314,6 +4314,16 @@ namespace z3 {
             Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
         }
 
+        void conflict(expr_vector const& fixed, expr_vector const& lhs, expr_vector const& rhs) {
+            assert(cb);
+            assert(lhs.size() == rhs.size());
+            expr conseq = ctx().bool_val(false);
+            array<Z3_ast> _fixed(fixed);
+            array<Z3_ast> _lhs(lhs);
+            array<Z3_ast> _rhs(rhs);
+            Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), lhs.size(), _lhs.ptr(), _rhs.ptr(), conseq);
+        }
+
         void propagate(expr_vector const& fixed, expr const& conseq) {
             assert(cb);
             assert((Z3_context)conseq.ctx() == (Z3_context)ctx());