Skip to content

Commit

Permalink
Fix default configuration for litmus tests (#720)
Browse files Browse the repository at this point in the history
Co-authored-by: Hernan Ponce de Leon <[email protected]>
  • Loading branch information
hernanponcedeleon and hernan-poncedeleon committed Aug 26, 2024
1 parent f6d10e2 commit 48d880d
Showing 1 changed file with 6 additions and 3 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -103,11 +103,14 @@ public BooleanFormula encodeBoundEventExec() {
public BooleanFormula encodeProperties(EnumSet<Property> properties) {
Property.Type specType = Property.getCombinedType(properties, context.getTask());
if (specType == Property.Type.MIXED) {
final String error = String.format(
final String warn = String.format(
"The set of properties %s are of mixed type (safety and reachability properties). " +
"Cannot encode mixed properties into a single SMT-query. Please select a different set of properties.",
"Cannot encode mixed properties into a single SMT-query. " +
"You can select a different set of properties with option --property. " +
"Defaulting to " + Property.PROGRAM_SPEC.asStringOption() + ".",
properties);
throw new IllegalArgumentException(error);
logger.warn(warn);
properties = EnumSet.of(Property.PROGRAM_SPEC);
}

BooleanFormula encoding = (specType == Property.Type.SAFETY) ?
Expand Down

0 comments on commit 48d880d

Please sign in to comment.