diff --git a/regression/cbmc/va_list2/main.c b/regression/cbmc/va_list2/main.c
index 90950aca44b..3be9e17c67b 100644
--- a/regression/cbmc/va_list2/main.c
+++ b/regression/cbmc/va_list2/main.c
@@ -11,14 +11,16 @@ void my_f(int first, ...)
 
   int v;
   v=__builtin_va_arg(args, int);
-  assert(v==2);
+  assert(v == 1);
+  v = __builtin_va_arg(args, int);
+  assert(v == 0);
 
   __builtin_va_end(args);
 }
 
 int main()
 {
-  my_f(1, 2);
+  my_f(2, 1, 0);
 }
 
 #else
diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp
index dc944e3d964..86e9790718b 100644
--- a/src/ansi-c/goto-conversion/builtin_functions.cpp
+++ b/src/ansi-c/goto-conversion/builtin_functions.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
 #include <util/pointer_expr.h>
+#include <util/pointer_offset_size.h>
 #include <util/rational.h>
 #include <util/rational_tools.h>
 #include <util/simplify_expr.h>
@@ -1306,12 +1307,24 @@ void goto_convertt::do_function_call_symbol(
         goto_programt::make_assignment(lhs, rhs, function.source_location()));
     }
 
-    code_assignt assign{
-      list_arg, plus_exprt{list_arg, from_integer(1, pointer_diff_type())}};
-    assign.rhs().set(
-      ID_C_va_arg_type, to_code_type(function.type()).return_type());
+    exprt rhs;
+    if(list_arg.type() == pointer_type(pointer_type(empty_typet{})))
+      rhs = plus_exprt{list_arg, from_integer(1, pointer_diff_type())};
+    else
+    {
+      // handle unexpected va_list types by just enforcing pointer increments by
+      // size-of-void*
+      rhs = typecast_exprt{
+        plus_exprt{
+          typecast_exprt{list_arg, pointer_type(char_type())},
+          from_integer(
+            *pointer_offset_size(pointer_type(empty_typet{}), ns),
+            pointer_diff_type())},
+        list_arg.type()};
+    }
+    rhs.set(ID_C_va_arg_type, to_code_type(function.type()).return_type());
     dest.add(goto_programt::make_assignment(
-      std::move(assign), function.source_location()));
+      list_arg, std::move(rhs), function.source_location()));
   }
   else if(identifier == "__builtin_va_copy")
   {