diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index dae4df445..c8fdfb51f 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -99,7 +99,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(args, a => a != null));
 
             Context.CheckContextMatch(args);
-            if (args.Length != NumArgs)
+            if (IsApp && args.Length != NumArgs)
                 throw new Z3Exception("Number of arguments does not match");
             NativeObject = Native.Z3_update_term(Context.nCtx, NativeObject, (uint)args.Length, Expr.ArrayToNative(args));
         }
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index 5c4f90920..f7edc6a2b 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -94,7 +94,7 @@ public class Expr extends AST
 	public void update(Expr[] args) throws Z3Exception
 	{
 		getContext().checkContextMatch(args);
-		if (args.length != getNumArgs())
+		if (isApp() && args.length != getNumArgs())
 			throw new Z3Exception("Number of arguments does not match");
 		setNativeObject(Native.updateTerm(getContext().nCtx(), getNativeObject(),
 				(int) args.length, Expr.arrayToNative(args)));