CBMC regression test label clash

[esteffin]

When writing a regression test .desc file and adding both gcc-only and new-smt-backend the former label is disregarded, so the test is run also when gcc is not the compiler.

Is there any work-around to honour both label?

What behaviour did you expect: the test is run with the new-smt-backend arguments only on gcc systems.
What happened instead: the test is run with the new-smt-backend arguments only on all system, failing.

[tautschnig]

Can you please share how you’ve invoked test.pl when observing this?

[tautschnig]

Doing some guessing: if it is about 9933b98, then perhaps the problem is that regression/cbmc/CMakeLists.txt lacks ${gcc_only_string} in "cbmc-new-smt-backend" (while regression/cbmc/Makefile does get this right). That's a but in the invocation of test.pl, not the script itself.