diff --git a/engine/builtin.go b/engine/builtin.go
index 3d64ab1c..5d58dd46 100644
--- a/engine/builtin.go
+++ b/engine/builtin.go
@@ -1418,9 +1418,9 @@ func writeTermOption(state *State, option Term, env *Env) (WriteOption, error) {
 		}
 
 		if o.Functor == "variable_names" {
-			vns := variableNames(o.Args[0], env)
-			if vns == nil {
-				return nil, DomainError(ValidDomainWriteOption, o, env)
+			vns, err := variableNames(o, env)
+			if err != nil {
+				return nil, err
 			}
 			return WithVariableNames(vns), nil
 		}
@@ -1457,31 +1457,58 @@ func writeTermOption(state *State, option Term, env *Env) (WriteOption, error) {
 	}
 }
 
-func variableNames(vnList Term, env *Env) map[Variable]Atom {
+func variableNames(option *Compound, env *Env) (map[Variable]Atom, error) {
 	vns := map[Variable]Atom{}
-	iter := ListIterator{List: vnList, Env: env}
+	iter := ListIterator{List: option.Args[0], Env: env}
 	for iter.Next() {
-		vn, ok := env.Resolve(iter.Current()).(*Compound)
-		if !ok || vn.Functor != "=" || len(vn.Args) != 2 {
-			return nil
+		var vn *Compound
+		switch elem := env.Resolve(iter.Current()).(type) {
+		case Variable:
+			return nil, InstantiationError(env)
+		case *Compound:
+			if elem.Functor != "=" || len(elem.Args) != 2 {
+				return nil, DomainError(ValidDomainWriteOption, option, env)
+			}
+			vn = elem
+		default:
+			return nil, DomainError(ValidDomainWriteOption, option, env)
 		}
-		n, ok := env.Resolve(vn.Args[0]).(Atom)
-		if !ok {
-			return nil
+
+		var n Atom
+		switch arg := env.Resolve(vn.Args[0]).(type) {
+		case Variable:
+			return nil, InstantiationError(env)
+		case Atom:
+			n = arg
+		default:
+			return nil, DomainError(ValidDomainWriteOption, option, env)
 		}
-		v, ok := env.Resolve(vn.Args[1]).(Variable)
-		if !ok {
-			return nil
+
+		var v Variable
+		switch arg := env.Resolve(vn.Args[1]).(type) {
+		case Variable:
+			v = arg
+		default:
+			return nil, DomainError(ValidDomainWriteOption, option, env)
 		}
+
 		if _, ok := vns[v]; ok {
 			continue
 		}
 		vns[v] = n
 	}
-	if err := iter.Err(); err != nil {
-		return nil
+
+	switch s := iter.Suffix().(type) {
+	case Variable:
+		return nil, InstantiationError(env)
+	case Atom:
+		if s != "[]" {
+			return nil, DomainError(ValidDomainWriteOption, option, env)
+		}
+		return vns, nil
+	default:
+		return nil, DomainError(ValidDomainWriteOption, option, env)
 	}
-	return vns
 }
 
 // CharCode converts a single-rune Atom char to an Integer code, or vice versa.
diff --git a/engine/builtin_test.go b/engine/builtin_test.go
index 536eeb32..20470a1e 100644
--- a/engine/builtin_test.go
+++ b/engine/builtin_test.go
@@ -4147,40 +4147,120 @@ func TestState_WriteTerm(t *testing.T) {
 			assert.Equal(t, 1200, m.priority)
 		})
 
-		t.Run("argument is not a proper list", func(t *testing.T) {
-			var m mockTerm
-			defer m.AssertExpectations(t)
+		t.Run("argument is not a list", func(t *testing.T) {
+			t.Run("partial list", func(t *testing.T) {
+				var m mockTerm
+				defer m.AssertExpectations(t)
+
+				_, err := state.WriteTerm(s, &m, List(&Compound{
+					Functor: "variable_names",
+					Args:    []Term{ListRest(Variable("L"), Atom("=").Apply(Atom("foo"), Variable("X")))},
+				}), Success, nil).Force(context.Background())
+				assert.Equal(t, InstantiationError(nil), err)
+			})
 
-			_, err := state.WriteTerm(s, &m, List(&Compound{
-				Functor: "variable_names",
-				Args:    []Term{Atom("=").Apply(Atom("foo"), Variable("X"))},
-			}), Success, nil).Force(context.Background())
-			assert.Error(t, err)
-			e, ok := err.(Exception)
-			assert.True(t, ok)
-			_, ok = e.term.Unify(DomainError(ValidDomainWriteOption, &Compound{
-				Functor: "variable_names",
-				Args:    []Term{Atom("=").Apply(Atom("foo"), Variable("X"))},
-			}, nil).term, false, nil)
-			assert.True(t, ok)
+			t.Run("suffix is atom", func(t *testing.T) {
+				var m mockTerm
+				defer m.AssertExpectations(t)
+
+				_, err := state.WriteTerm(s, &m, List(&Compound{
+					Functor: "variable_names",
+					Args:    []Term{ListRest(Atom("rest"), Atom("=").Apply(Atom("foo"), Variable("X")))},
+				}), Success, nil).Force(context.Background())
+				e, ok := err.(Exception)
+				assert.True(t, ok)
+				_, ok = e.term.Unify(DomainError(ValidDomainWriteOption, &Compound{
+					Functor: "variable_names",
+					Args:    []Term{ListRest(Atom("rest"), Atom("=").Apply(Atom("foo"), Variable("X")))},
+				}, nil).term, false, nil)
+				assert.True(t, ok)
+			})
+
+			t.Run("suffix is compound", func(t *testing.T) {
+				var m mockTerm
+				defer m.AssertExpectations(t)
+
+				_, err := state.WriteTerm(s, &m, List(&Compound{
+					Functor: "variable_names",
+					Args:    []Term{Atom("=").Apply(Atom("foo"), Variable("X"))},
+				}), Success, nil).Force(context.Background())
+				assert.Error(t, err)
+				e, ok := err.(Exception)
+				assert.True(t, ok)
+				_, ok = e.term.Unify(DomainError(ValidDomainWriteOption, &Compound{
+					Functor: "variable_names",
+					Args:    []Term{Atom("=").Apply(Atom("foo"), Variable("X"))},
+				}, nil).term, false, nil)
+				assert.True(t, ok)
+			})
 		})
 
-		t.Run("element is not name=variable", func(t *testing.T) {
-			var m mockTerm
-			defer m.AssertExpectations(t)
+		t.Run("element is not name=Variable", func(t *testing.T) {
+			t.Run("a variable", func(t *testing.T) {
+				var m mockTerm
+				defer m.AssertExpectations(t)
 
-			_, err := state.WriteTerm(s, &m, List(&Compound{
-				Functor: "variable_names",
-				Args: []Term{List(
-					Atom("foo"),
-				)},
-			}), Success, nil).Force(context.Background())
-			assert.Equal(t, DomainError(ValidDomainWriteOption, &Compound{
-				Functor: "variable_names",
-				Args: []Term{List(
-					Atom("foo"),
-				)},
-			}, nil), err)
+				_, err := state.WriteTerm(s, &m, List(&Compound{
+					Functor: "variable_names",
+					Args: []Term{List(
+						Variable("VN"),
+					)},
+				}), Success, nil).Force(context.Background())
+				assert.Equal(t, InstantiationError(nil), err)
+			})
+
+			t.Run("a compound which is not =/2", func(t *testing.T) {
+				var m mockTerm
+				defer m.AssertExpectations(t)
+
+				_, err := state.WriteTerm(s, &m, List(&Compound{
+					Functor: "variable_names",
+					Args: []Term{List(
+						Atom("foo").Apply(Atom("n"), Variable("V")),
+					)},
+				}), Success, nil).Force(context.Background())
+				assert.Error(t, err)
+				e, ok := err.(Exception)
+				assert.True(t, ok)
+				_, ok = e.term.Unify(DomainError(ValidDomainWriteOption, &Compound{
+					Functor: "variable_names",
+					Args: []Term{List(
+						Atom("foo").Apply(Atom("n"), Variable("V")),
+					)},
+				}, nil).term, false, nil)
+				assert.True(t, ok)
+			})
+
+			t.Run("a compound of =/2 but lhs is not an atom", func(t *testing.T) {
+				var m mockTerm
+				defer m.AssertExpectations(t)
+
+				_, err := state.WriteTerm(s, &m, List(&Compound{
+					Functor: "variable_names",
+					Args: []Term{List(
+						Atom("=").Apply(Variable("N"), Variable("V")),
+					)},
+				}), Success, nil).Force(context.Background())
+				assert.Equal(t, InstantiationError(nil), err)
+			})
+
+			t.Run("neither a variable nor a compound", func(t *testing.T) {
+				var m mockTerm
+				defer m.AssertExpectations(t)
+
+				_, err := state.WriteTerm(s, &m, List(&Compound{
+					Functor: "variable_names",
+					Args: []Term{List(
+						Atom("foo"),
+					)},
+				}), Success, nil).Force(context.Background())
+				assert.Equal(t, DomainError(ValidDomainWriteOption, &Compound{
+					Functor: "variable_names",
+					Args: []Term{List(
+						Atom("foo"),
+					)},
+				}, nil), err)
+			})
 		})
 
 		t.Run("name is not an atom", func(t *testing.T) {