Merge branch 'development_rework' into fixes

README.md

@@ -90,7 +90,7 @@ You can also run Dartagnan from the console:
 ```
 java -jar dartagnan/target/dartagnan-3.1.1.jar <CAT file> [--target=<arch>] <program file> [options]
 ```
-For programs written in `.c` and `.bpl`, value `<arch>` specifies the programming language or architectures to which the program will be compiled. Program written in `.litmus` format do not require such option. `<arch>` must be one of the following: 
+For programs written in `.c` and `.bpl`, value `<arch>` specifies the programming language or architectures to which the program will be compiled. For programs written in `.litmus` format, if the `--target` option is not given, Dartagnan will automatically extract the `<arch>` from the litmus test header. `<arch>` must be one of the following: 
 - c11
 - lkmm
 - imm

dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java

@@ -17,6 +17,7 @@
 import com.dat3m.dartagnan.utils.Result;
 import com.dat3m.dartagnan.utils.options.BaseOptions;
 import com.dat3m.dartagnan.verification.VerificationTask;
+import com.dat3m.dartagnan.verification.VerificationTask.VerificationTaskBuilder;
 import com.dat3m.dartagnan.verification.model.ExecutionModel;
 import com.dat3m.dartagnan.verification.solving.*;
 import com.dat3m.dartagnan.witness.WitnessBuilder;
@@ -46,6 +47,7 @@
 import static com.dat3m.dartagnan.GlobalSettings.LogGlobalSettings;
 import static com.dat3m.dartagnan.configuration.OptionInfo.collectOptions;
 import static com.dat3m.dartagnan.configuration.OptionNames.PHANTOM_REFERENCES;
+import static com.dat3m.dartagnan.configuration.OptionNames.TARGET;;
 import static com.dat3m.dartagnan.configuration.Property.*;
 import static com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis.*;
 import static com.dat3m.dartagnan.utils.GitInfo.CreateGitInfo;
@@ -109,10 +111,16 @@ public static void main(String[] args) throws Exception {
             witness = new ParserWitness().parse(new File(o.getWitnessPath()));
         }
 
-        VerificationTask task = VerificationTask.builder()
+        VerificationTaskBuilder builder = VerificationTask.builder()
                 .withConfig(config)
-                .withWitness(witness)
-                .build(p, mcm, properties);
+                .withWitness(witness);
+        // If the arch has been set during parsing (this only happens for litmus tests)
+        // and the user did not explicitly add the target option, we use the one
+        // obtained during parsing.
+        if (p.getArch() != null && !config.hasProperty(TARGET)) {
+            builder = builder.withTarget(p.getArch());
+        }
+        VerificationTask task = builder.build(p, mcm, properties);
 
         ShutdownManager sdm = ShutdownManager.create();
         Thread t = new Thread(() -> {