From 48d880d4a8c524f1275c003a4e2a305f1d0dcbc7 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 26 Aug 2024 12:28:58 +0200 Subject: [PATCH] Fix default configuration for litmus tests (#720) Co-authored-by: Hernan Ponce de Leon --- .../com/dat3m/dartagnan/encoding/PropertyEncoder.java | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) 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) ?