diff --git a/regression/goto-gcc/at_files/args b/regression/goto-gcc/at_files/args
new file mode 100644
index 00000000000..c151b9c1fb2
--- /dev/null
+++ b/regression/goto-gcc/at_files/args
@@ -0,0 +1 @@
+other.c
diff --git a/regression/goto-gcc/at_files/main.c b/regression/goto-gcc/at_files/main.c
new file mode 100644
index 00000000000..5be0864eeee
--- /dev/null
+++ b/regression/goto-gcc/at_files/main.c
@@ -0,0 +1,6 @@
+int foo();
+
+int main()
+{
+  return foo();
+}
diff --git a/regression/goto-gcc/at_files/other.c b/regression/goto-gcc/at_files/other.c
new file mode 100644
index 00000000000..0ced01a564d
--- /dev/null
+++ b/regression/goto-gcc/at_files/other.c
@@ -0,0 +1,4 @@
+int foo()
+{
+  return 1;
+}
diff --git a/regression/goto-gcc/at_files/test.desc b/regression/goto-gcc/at_files/test.desc
new file mode 100644
index 00000000000..eb31709f0f3
--- /dev/null
+++ b/regression/goto-gcc/at_files/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+@args
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/src/goto-cc/gcc_cmdline.cpp b/src/goto-cc/gcc_cmdline.cpp
index e4b2bb1ddb6..893ccc0452a 100644
--- a/src/goto-cc/gcc_cmdline.cpp
+++ b/src/goto-cc/gcc_cmdline.cpp
@@ -252,7 +252,7 @@ bool gcc_cmdlinet::parse_arguments(
         line.erase(0, line.find_first_not_of("\t "));
 
         if(!line.empty())
-          parse_specs_line(line);
+          parse_specs_line(line, false);
       }
 
       continue;
@@ -428,7 +428,7 @@ bool gcc_cmdlinet::parse_arguments(
 }
 
 /// Parse GCC spec files https://gcc.gnu.org/onlinedocs/gcc/Spec-Files.html
-void gcc_cmdlinet::parse_specs_line(const std::string &line)
+void gcc_cmdlinet::parse_specs_line(const std::string &line, bool in_spec_file)
 {
   // initial whitespace has been stripped
   assert(!line.empty());
@@ -444,7 +444,7 @@ void gcc_cmdlinet::parse_specs_line(const std::string &line)
     args.push_back(line.substr(arg_start, arg_end-arg_start));
   }
 
-  parse_arguments(args, true);
+  parse_arguments(args, in_spec_file);
 }
 
 /// Parse GCC spec files https://gcc.gnu.org/onlinedocs/gcc/Spec-Files.html
@@ -473,7 +473,7 @@ void gcc_cmdlinet::parse_specs()
              line=="*link:"))
       use_line=true;
     else if(use_line)
-      parse_specs_line(line);
+      parse_specs_line(line, true);
     else
     {
       // TODO need message interface
diff --git a/src/goto-cc/gcc_cmdline.h b/src/goto-cc/gcc_cmdline.h
index 92ac348118c..6afc77fd39f 100644
--- a/src/goto-cc/gcc_cmdline.h
+++ b/src/goto-cc/gcc_cmdline.h
@@ -31,7 +31,7 @@ class gcc_cmdlinet:public goto_cc_cmdlinet
 
   bool parse_arguments(const argst &args, bool in_spec_file);
   void parse_specs();
-  void parse_specs_line(const std::string &line);
+  void parse_specs_line(const std::string &line, bool in_spec_file);
 };
 
 #endif // CPROVER_GOTO_CC_GCC_CMDLINE_H