Skip to content

Commit 32e10c8

Browse files
Generate SVCOMP witness if PROGRAM_SPEC is the only property (#615)
Signed-off-by: Hernan Ponce de Leon <[email protected]>
1 parent c5b4d91 commit 32e10c8

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -215,7 +215,7 @@ private static void generateWitnessIfAble(VerificationTask task, ProverEnvironme
215215
// ------------------ Generate Witness, if possible ------------------
216216
final EnumSet<Property> properties = task.getProperty();
217217
if (task.getProgram().getFormat().equals(SourceLanguage.LLVM) && modelChecker.hasModel()
218-
&& properties.contains(PROGRAM_SPEC)) {
218+
&& properties.contains(PROGRAM_SPEC) && properties.size() == 1) {
219219
try {
220220
WitnessBuilder w = WitnessBuilder.of(modelChecker.getEncodingContext(), prover,
221221
modelChecker.getResult(), summary);

0 commit comments

Comments
 (0)