expr utilities for pb

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/dotnet/Expr.cs

@@ -89,6 +89,15 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// The i'th argument of the expression.
+        /// </summary>
+        public Expr Arg(uint i)
+        {
+            Contract.Ensures(Contract.Result<Expr>() != null);
+            return Expr.Create(Context, Native.Z3_get_app_arg(Context.nCtx, NativeObject, i));
+        }
+
         /// <summary>
         /// Update the arguments of the expression using the arguments <paramref name="args"/>
         /// The number of new arguments should coincide with the current number of arguments.
@@ -315,6 +324,41 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsImplies { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } }
 
+        /// <summary>
+        /// Indicates whether the term is at-most
+        /// </summary>
+        public bool IsAtMost { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_AT_MOST; } }
+
+        /// <summary>
+        /// Retrieve bound of at-most
+        /// </summary>
+        public uint AtMostBound { get { Contract.Requires(IsAtMost); return (uint)FuncDecl.Parameters[0].Int; } }
+
+        /// <summary>
+        /// Indicates whether the term is at-least
+        /// </summary>
+        public bool IsAtLeast { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_AT_LEAST; } }
+
+        /// <summary>
+        /// Retrieve bound of at-least
+        /// </summary>
+        public uint AtLeastBound { get { Contract.Requires(IsAtLeast); return (uint)FuncDecl.Parameters[0].Int; } }
+
+        /// <summary>
+        /// Indicates whether the term is pbeq
+        /// </summary>
+        public bool IsPbEq { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_EQ; } }
+
+        /// <summary>
+        /// Indicates whether the term is pble
+        /// </summary>
+        public bool IsPbLe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_LE; } }
+
+        /// <summary>
+        /// Indicates whether the term is pbge
+        /// </summary>
+        public bool IsPbGe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_GE; } }        
+
         #endregion
 
         #region Arithmetic Terms

src/sat/ba_solver.cpp

@@ -1976,6 +1976,7 @@ namespace sat {
             for (unsigned i = 0; !found && i < c.k(); ++i) {
                 found = c[i] == l;
             }
+            CTRACE("ba",!found, tout << l << ": " << c << "\n";);
             SASSERT(found););
         
         // IF_VERBOSE(0, if (_debug_conflict) verbose_stream() << "ante " << l << " " << c << "\n");