Call witness builder only for LLVM code (#593)

Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>
hernanponcedeleon · Dec 20, 2023 · ad48350 · ad48350
1 parent c977cbc
commit ad48350
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java
@@ -218,7 +218,7 @@ public static void main(String[] args) throws Exception {
     private static void generateWitnessIfAble(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker, String summary) {
         // ------------------ Generate Witness, if possible ------------------
         final EnumSet<Property> properties = task.getProperty();
-        if (modelChecker.hasModel() && properties.contains(PROGRAM_SPEC)) {
+        if (task.getProgram().getFormat().equals(SourceLanguage.LLVM) && modelChecker.hasModel() && properties.contains(PROGRAM_SPEC)) {
             try {
                 WitnessBuilder w = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, modelChecker.getResult(), summary);
                 if (w.canBeBuilt()) {