From 811cd9d48d98963be64e730e5a61a4b310bfee3a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 3 Mar 2022 09:14:47 -0800
Subject: [PATCH] add example

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/NativeSolver.cs | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/api/dotnet/NativeSolver.cs b/src/api/dotnet/NativeSolver.cs
index 74238692f..01e761e18 100644
--- a/src/api/dotnet/NativeSolver.cs
+++ b/src/api/dotnet/NativeSolver.cs
@@ -200,6 +200,11 @@ namespace Microsoft.Z3
 
         /// <summary>
         /// Add constraints to ensure the function f can only be injective.
+        /// Example:
+        /// for function f : D1 x D2 -> R
+        /// assert axioms
+        ///   forall (x1 : D1, x2 : D2) x1 = inv1(f(x1,x2))
+        ///   forall (x1 : D1, x2 : D2) x2 = inv2(f(x1,x2))
         /// </summary>
         /// <param name="f"></param>
         public void AssertInjective(Z3_func_decl f)