diff --git a/src/api/dotnet/UserPropagator.cs b/src/api/dotnet/UserPropagator.cs
index cd8fa3ba5..eb181b272 100644
--- a/src/api/dotnet/UserPropagator.cs
+++ b/src/api/dotnet/UserPropagator.cs
@@ -37,280 +37,306 @@ namespace Microsoft.Z3
     /// <summary>
     /// Propagator context for .Net
     /// </summary>        
-    public class UserPropagator 
+    public class UserPropagator
     {
         /// <summary>
         /// Delegate type for fixed callback
         /// </summary>                
-	public delegate void FixedEh(Expr term, Expr value);
+        public delegate void FixedEh(Expr term, Expr value);
 
         /// <summary>
         /// Delegate type for equality or disequality callback
         /// </summary>                
-	public delegate void EqEh(Expr term, Expr value);
+        public delegate void EqEh(Expr term, Expr value);
 
         /// <summary>
         /// Delegate type for when a new term using a registered function symbol is created internally
         /// </summary>                
-	public delegate void CreatedEh(Expr term);
+        public delegate void CreatedEh(Expr term);
 
         /// <summary>
         /// Delegate type for callback into solver's branching
-	/// <param name="term">A bit-vector or Boolean used for branching</param>
-	/// <param name="idx">If the term is a bit-vector, then an index into the bit-vector being branched on</param>
-	/// <param name="phase">Set phase to -1 (false) or 1 (true) to override solver's phase</param>
-	/// </summary>                
-	public delegate void DecideEh(ref Expr term, ref uint idx, ref int phase);
+        /// <param name="term">A bit-vector or Boolean used for branching</param>
+        /// <param name="idx">If the term is a bit-vector, then an index into the bit-vector being branched on</param>
+        /// <param name="phase">Set phase to -1 (false) or 1 (true) to override solver's phase</param>
+        /// </summary>                
+        public delegate void DecideEh(ref Expr term, ref uint idx, ref int phase);
 
         // access managed objects through a static array.
-	// thread safety is ignored for now.
-	static List<UserPropagator> propagators = new List<UserPropagator>();
-	int      id;
-	Solver   solver;
-	Context  ctx;
-	Z3_solver_callback callback = IntPtr.Zero;
-	FixedEh fixed_eh;
-	Action  final_eh;
-	EqEh    eq_eh;
-	EqEh    diseq_eh;
-	CreatedEh created_eh;
-	DecideEh  decide_eh;
+        // thread safety is ignored for now.
+        static List<UserPropagator> propagators = new List<UserPropagator>();
+        int id;
+        Solver solver;
+        Context ctx;
+        Z3_solver_callback callback = IntPtr.Zero;
+        FixedEh fixed_eh;
+        Action final_eh;
+        EqEh eq_eh;
+        EqEh diseq_eh;
+        CreatedEh created_eh;
+        DecideEh decide_eh;
 
-	void Callback(Action fn, Z3_solver_callback cb) {
-	    this.callback = cb;
-	    try {	    
-	        fn();
-	    }
-	    catch {
-	        // TBD: add debug log or exception handler		
-	    }
-	    finally {
-	       this.callback = IntPtr.Zero;
-	    }
-	}
+        void Callback(Action fn, Z3_solver_callback cb)
+        {
+            this.callback = cb;
+            try
+            {
+                fn();
+            }
+            catch
+            {
+                // TBD: add debug log or exception handler		
+            }
+            finally
+            {
+                this.callback = IntPtr.Zero;
+            }
+        }
 
 
-	static void _push(voidp ctx, Z3_solver_callback cb) {
-	   var prop = propagators[ctx.ToInt32()];
-	   prop.Callback(() => prop.Push(), cb);
-	}
-	
-	static void _pop(voidp ctx, Z3_solver_callback cb, uint num_scopes) {
-	   var prop = propagators[ctx.ToInt32()];
-	   prop.Callback(() => prop.Pop(num_scopes), cb);
-	}
-	
-	static voidp _fresh(voidp _ctx, Z3_context new_context) {
-	   var prop = propagators[_ctx.ToInt32()];
-           var ctx = new Context(new_context);
-           var prop1 = prop.Fresh(prop.ctx);
-           return new IntPtr(prop1.id);
-	}
+        static void _push(voidp ctx, Z3_solver_callback cb)
+        {
+            var prop = propagators[ctx.ToInt32()];
+            prop.Callback(() => prop.Push(), cb);
+        }
 
-	static void _fixed(voidp ctx, Z3_solver_callback cb, Z3_ast _term, Z3_ast _value) {
-           var prop = propagators[ctx.ToInt32()];
-	   using var term = Expr.Create(prop.ctx, _term);
-	   using var value = Expr.Create(prop.ctx, _value);
-	   prop.Callback(() => prop.fixed_eh(term, value), cb);
-	}
+        static void _pop(voidp ctx, Z3_solver_callback cb, uint num_scopes)
+        {
+            var prop = propagators[ctx.ToInt32()];
+            prop.Callback(() => prop.Pop(num_scopes), cb);
+        }
 
-	static void _final(voidp ctx, Z3_solver_callback cb) {
-           var prop = propagators[ctx.ToInt32()];
-	   prop.Callback(() => prop.final_eh(), cb);
-	}
+        static voidp _fresh(voidp _ctx, Z3_context new_context)
+        {
+            var prop = propagators[_ctx.ToInt32()];
+            var ctx = new Context(new_context);
+            var prop1 = prop.Fresh(prop.ctx);
+            return new IntPtr(prop1.id);
+        }
 
-	static void _eq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) {
-           var prop = propagators[ctx.ToInt32()];
-	   using var s = Expr.Create(prop.ctx, a);
-	   using var t = Expr.Create(prop.ctx, b);
-	   prop.Callback(() => prop.eq_eh(s, t), cb);
-	}
+        static void _fixed(voidp ctx, Z3_solver_callback cb, Z3_ast _term, Z3_ast _value)
+        {
+            var prop = propagators[ctx.ToInt32()];
+            using var term = Expr.Create(prop.ctx, _term);
+            using var value = Expr.Create(prop.ctx, _value);
+            prop.Callback(() => prop.fixed_eh(term, value), cb);
+        }
 
-	static void _diseq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) {
-           var prop = propagators[ctx.ToInt32()];
-	   using var s = Expr.Create(prop.ctx, a);
-	   using var t = Expr.Create(prop.ctx, b);
-	   prop.Callback(() => prop.diseq_eh(s, t), cb);
-	}
+        static void _final(voidp ctx, Z3_solver_callback cb)
+        {
+            var prop = propagators[ctx.ToInt32()];
+            prop.Callback(() => prop.final_eh(), cb);
+        }
 
-	static void _created(voidp ctx, Z3_solver_callback cb, Z3_ast a) {
-           var prop = propagators[ctx.ToInt32()];
-	   using var t = Expr.Create(prop.ctx, a);
-	   prop.Callback(() => prop.created_eh(t), cb);
-	}
+        static void _eq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b)
+        {
+            var prop = propagators[ctx.ToInt32()];
+            using var s = Expr.Create(prop.ctx, a);
+            using var t = Expr.Create(prop.ctx, b);
+            prop.Callback(() => prop.eq_eh(s, t), cb);
+        }
 
-	static void _decide(voidp ctx, Z3_solver_callback cb, ref Z3_ast a, ref uint idx, ref int phase) {
-           var prop = propagators[ctx.ToInt32()];
-	   var t = Expr.Create(prop.ctx, a);
-	   var u = t;
-	   prop.callback = cb;
-	   prop.decide_eh(ref t, ref idx, ref phase);
-	   prop.callback = IntPtr.Zero;
-	   if (u != t) 
-	       a = t.NativeObject;
-	}
+        static void _diseq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b)
+        {
+            var prop = propagators[ctx.ToInt32()];
+            using var s = Expr.Create(prop.ctx, a);
+            using var t = Expr.Create(prop.ctx, b);
+            prop.Callback(() => prop.diseq_eh(s, t), cb);
+        }
+
+        static void _created(voidp ctx, Z3_solver_callback cb, Z3_ast a)
+        {
+            var prop = propagators[ctx.ToInt32()];
+            using var t = Expr.Create(prop.ctx, a);
+            prop.Callback(() => prop.created_eh(t), cb);
+        }
+
+        static void _decide(voidp ctx, Z3_solver_callback cb, ref Z3_ast a, ref uint idx, ref int phase)
+        {
+            var prop = propagators[ctx.ToInt32()];
+            var t = Expr.Create(prop.ctx, a);
+            var u = t;
+            prop.callback = cb;
+            prop.decide_eh(ref t, ref idx, ref phase);
+            prop.callback = IntPtr.Zero;
+            if (u != t)
+                a = t.NativeObject;
+        }
 
         /// <summary>
         /// Propagator constructor from a solver class.
         /// </summary>        
         public UserPropagator(Solver s)
-	{
-	    id = propagators.Count;
-	    propagators.Add(this);
-	    solver = s;
-	    ctx = solver.Context;
-	    Native.Z3_solver_propagate_init(ctx.nCtx, solver.NativeObject, new IntPtr(id), _push, _pop, _fresh);
-	}
+        {
+            id = propagators.Count;
+            propagators.Add(this);
+            solver = s;
+            ctx = solver.Context;
+            Native.Z3_solver_propagate_init(ctx.nCtx, solver.NativeObject, new IntPtr(id), _push, _pop, _fresh);
+        }
 
         /// <summary>
         /// Propagator constructor from a context. It is used from inside of Fresh.
         /// </summary>        
         public UserPropagator(Context _ctx)
-	{
-	    id = propagators.Count;
-	    propagators.Add(this);
+        {
+            id = propagators.Count;
+            propagators.Add(this);
             solver = null;
-	    ctx = _ctx;
-	}
+            ctx = _ctx;
+        }
 
         /// <summary>
         /// Release provate memory.
         /// </summary>            
-	~UserPropagator()
-	{
+        ~UserPropagator()
+        {
             propagators[id] = null;
             if (solver == null)
                 ctx.Dispose();
- 	}
+        }
 
         /// <summary>
         /// Virtual method for push. It must be overwritten by inherited class.
-	/// </summary>        
-	public virtual void Push() { throw new Z3Exception("Push method should be overwritten"); }
+        /// </summary>        
+        public virtual void Push() { throw new Z3Exception("Push method should be overwritten"); }
 
         /// <summary>
         /// Virtual method for pop. It must be overwritten by inherited class.
-	/// </summary>        
-	public virtual void Pop(uint n) { throw new Z3Exception("Pop method should be overwritten"); } 
+        /// </summary>        
+        public virtual void Pop(uint n) { throw new Z3Exception("Pop method should be overwritten"); }
 
         /// <summary>
         /// Virtual method for fresh. It can be overwritten by inherited class.
-	/// </summary>
-	public virtual UserPropagator Fresh(Context ctx) { return new UserPropagator(ctx); }
+        /// </summary>
+        public virtual UserPropagator Fresh(Context ctx) { return new UserPropagator(ctx); }
 
         /// <summary>
         /// Declare combination of assigned expressions a conflict
-	/// </summary>
-        public void Conflict(params Expr[] terms) {
-             Propagate(terms, ctx.MkFalse());
+        /// </summary>
+        public void Conflict(params Expr[] terms)
+        {
+            Propagate(terms, ctx.MkFalse());
+        }
+
+        /// <summary>
+        /// Declare combination of assigned expressions a conflict
+        /// </summary>
+        public void Conflict(IEnumerable<Expr> terms)
+        {
+            Propagate(terms, ctx.MkFalse());
         }
 
         /// <summary>
         /// Propagate consequence
-	/// </summary>
-        public void Propagate(Expr[] terms, Expr conseq) {
-            var nTerms = Z3Object.ArrayToNative(terms);
+        /// </summary>
+        public void Propagate(IEnumerable<Expr> terms, Expr conseq)
+        {
+            var nTerms = Z3Object.ArrayToNative(terms.ToArray());
             Native.Z3_solver_propagate_consequence(ctx.nCtx, this.callback, (uint)nTerms.Length, nTerms, 0u, null, null, conseq.NativeObject);
         }
 
 
         /// <summary>
         /// Set fixed callback
-	/// </summary>
+        /// </summary>
         public FixedEh Fixed
-	{
-	    set
-	    {
-	       this.fixed_eh = value;
-               if (solver != null)
-                   Native.Z3_solver_propagate_fixed(ctx.nCtx, solver.NativeObject, _fixed);
-	    }
-	}
+        {
+            set
+            {
+                this.fixed_eh = value;
+                if (solver != null)
+                    Native.Z3_solver_propagate_fixed(ctx.nCtx, solver.NativeObject, _fixed);
+            }
+        }
 
         /// <summary>
         /// Set final callback
-	/// </summary>
-	public Action Final
-	{
-	    set
-	    {
-	       this.final_eh = value;
-               if (solver != null)
- 	          Native.Z3_solver_propagate_final(ctx.nCtx, solver.NativeObject, _final);
+        /// </summary>
+        public Action Final
+        {
+            set
+            {
+                this.final_eh = value;
+                if (solver != null)
+                    Native.Z3_solver_propagate_final(ctx.nCtx, solver.NativeObject, _final);
             }
         }
 
         /// <summary>
         /// Set equality event callback
-	/// </summary>
-	public EqEh Eq
-	{
-           set
-	   {
- 	      this.eq_eh = value;
-              if (solver != null)
-  	         Native.Z3_solver_propagate_eq(ctx.nCtx, solver.NativeObject, _eq);
-	   }
+        /// </summary>
+        public EqEh Eq
+        {
+            set
+            {
+                this.eq_eh = value;
+                if (solver != null)
+                    Native.Z3_solver_propagate_eq(ctx.nCtx, solver.NativeObject, _eq);
+            }
         }
 
         /// <summary>
         /// Set disequality event callback
-	/// </summary>
-	public EqEh Diseq
-	{
-           set
-	   {
- 	      this.diseq_eh = value;
-              if (solver != null)
-                 Native.Z3_solver_propagate_diseq(ctx.nCtx, solver.NativeObject, _diseq);
-	   }
+        /// </summary>
+        public EqEh Diseq
+        {
+            set
+            {
+                this.diseq_eh = value;
+                if (solver != null)
+                    Native.Z3_solver_propagate_diseq(ctx.nCtx, solver.NativeObject, _diseq);
+            }
         }
 
         /// <summary>
         /// Set created callback
-	/// </summary>
-	public CreatedEh Created
-	{
-           set
-	   {
- 	      this.created_eh = value;
-              if (solver != null)
-                  Native.Z3_solver_propagate_created(ctx.nCtx, solver.NativeObject, _created);
-	   }
+        /// </summary>
+        public CreatedEh Created
+        {
+            set
+            {
+                this.created_eh = value;
+                if (solver != null)
+                    Native.Z3_solver_propagate_created(ctx.nCtx, solver.NativeObject, _created);
+            }
         }
 
         /// <summary>
         /// Set decision callback
-	/// </summary>
-	public DecideEh Decide
-	{
-           set
-	   {
- 	      this.decide_eh = value;
-              if (solver != null)
-                  Native.Z3_solver_propagate_decide(ctx.nCtx, solver.NativeObject, _decide);
-	   }
+        /// </summary>
+        public DecideEh Decide
+        {
+            set
+            {
+                this.decide_eh = value;
+                if (solver != null)
+                    Native.Z3_solver_propagate_decide(ctx.nCtx, solver.NativeObject, _decide);
+            }
         }
 
-       
+
         /// <summary>
         /// Set the next decision
-	/// </summary>
-	public void NextSplit(Expr e, uint idx, int phase)
-	{
-           Native.Z3_solver_next_split(ctx.nCtx, this.callback, e.NativeObject, idx, phase);
-	}
+        /// </summary>
+        public void NextSplit(Expr e, uint idx, int phase)
+        {
+            Native.Z3_solver_next_split(ctx.nCtx, this.callback, e.NativeObject, idx, phase);
+        }
 
         /// <summary>
         /// Track assignments to a term
-	/// </summary>
-        public void Register(Expr term) {
-            if (this.callback != IntPtr.Zero) {
-               Native.Z3_solver_propagate_register_cb(ctx.nCtx, callback, term.NativeObject);
+        /// </summary>
+        public void Register(Expr term)
+        {
+            if (this.callback != IntPtr.Zero)
+            {
+                Native.Z3_solver_propagate_register_cb(ctx.nCtx, callback, term.NativeObject);
             }
-            else {
-               Native.Z3_solver_propagate_register(ctx.nCtx, solver.NativeObject, term.NativeObject);
+            else
+            {
+                Native.Z3_solver_propagate_register(ctx.nCtx, solver.NativeObject, term.NativeObject);
             }
-        }	
+        }
     }
 }