diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java index 398a34d5bf..fa7ed2b267 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java @@ -103,11 +103,14 @@ public BooleanFormula encodeBoundEventExec() { public BooleanFormula encodeProperties(EnumSet 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) ?