diff --git a/regression/goto-instrument/nondet-volatile-01/test.c b/regression/goto-instrument/nondet-volatile-01/test.c
new file mode 100644
index 00000000000..ec0cc273a79
--- /dev/null
+++ b/regression/goto-instrument/nondet-volatile-01/test.c
@@ -0,0 +1,11 @@
+#include <assert.h>
+
+void main()
+{
+  int a[2] = {0};
+
+  volatile int i = 0;
+  a[i] = 1;
+
+  assert(a[1] == 0); // should fail
+}
diff --git a/regression/goto-instrument/nondet-volatile-01/test.desc b/regression/goto-instrument/nondet-volatile-01/test.desc
new file mode 100644
index 00000000000..06b61f44592
--- /dev/null
+++ b/regression/goto-instrument/nondet-volatile-01/test.desc
@@ -0,0 +1,9 @@
+CORE
+test.c
+--nondet-volatile
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Check that volatile variables appearing in the lhs of an assignment are
+correctly treated as nondet
diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-instrument/nondet_volatile.cpp
index 73a79937355..96514c144e3 100644
--- a/src/goto-instrument/nondet_volatile.cpp
+++ b/src/goto-instrument/nondet_volatile.cpp
@@ -31,7 +31,7 @@ static bool is_volatile(const namespacet &ns, const typet &src)
   return false;
 }
 
-void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
+static void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
 {
   Forall_operands(it, expr)
     nondet_volatile_rhs(symbol_table, *it);
@@ -52,7 +52,7 @@ void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
   }
 }
 
-void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
+static void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
 {
   if(expr.id()==ID_if)
   {
@@ -75,9 +75,8 @@ void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
   }
 }
 
-void nondet_volatile(
-  symbol_tablet &symbol_table,
-  goto_programt &goto_program)
+static void
+nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
 {
   namespacet ns(symbol_table);
 
@@ -88,7 +87,7 @@ void nondet_volatile(
     if(instruction.is_assign())
     {
       nondet_volatile_rhs(symbol_table, to_code_assign(instruction.code).rhs());
-      nondet_volatile_lhs(symbol_table, to_code_assign(instruction.code).rhs());
+      nondet_volatile_lhs(symbol_table, to_code_assign(instruction.code).lhs());
     }
     else if(instruction.is_function_call())
     {
diff --git a/src/goto-instrument/nondet_volatile.h b/src/goto-instrument/nondet_volatile.h
index dd92f3b1833..931478e96d1 100644
--- a/src/goto-instrument/nondet_volatile.h
+++ b/src/goto-instrument/nondet_volatile.h
@@ -14,10 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/goto_model.h>
 
-bool is_volatile(
-  const symbol_tablet &,
-  const typet &);
-
 void nondet_volatile(goto_modelt &);
 
 #endif // CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H