From d66f0c22ea43b3d88b843746f8975372ef22f722 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 24 Jul 2024 22:54:14 +0200
Subject: [PATCH] compiletest: ensure extra arguments are appended at the end
 (#3379)

We must not mix arguments to be passed to Kani with those parsed by
compiletest. Will enable use of `--cbmc-args` to increase CBMC's
verbosity as needed for certain tests.
---
 tools/compiletest/src/runtest.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs
index 7925ed83e6e5..50f1e3035ac8 100644
--- a/tools/compiletest/src/runtest.rs
+++ b/tools/compiletest/src/runtest.rs
@@ -272,14 +272,14 @@ impl<'test> TestCx<'test> {
             .arg("kani")
             .arg("--target-dir")
             .arg(self.output_base_dir().join("target"))
-            .current_dir(parent_dir)
-            .args(&self.config.extra_args);
+            .current_dir(parent_dir);
         if test {
             cargo.arg("--tests");
         }
         if "expected" != self.testpaths.file.file_name().unwrap() {
             cargo.args(["--harness", function_name]);
         }
+        cargo.args(&self.config.extra_args);
 
         let proc_res = self.compose_and_run(cargo);
         self.verify_output(&proc_res, &self.testpaths.file);