diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 718ac152e4..40a0e0c135 100644 --- 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()) {