From 9f1c540f050bc3f70ea12e1f8570f381bf1d30f1 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 19 Apr 2021 12:26:51 +0200 Subject: [PATCH] Counterexamples:making minimal label set generator aware of unbounded integer variables --- .../counterexamples/SMTMinimalLabelSetGenerator.h | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index 609bd8d50..6459be5d1 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -423,13 +423,11 @@ namespace storm { // Then add the constraints for bounds of the integer variables. for (auto const& integerVariable : program.getGlobalIntegerVariables()) { - localSolver->add(integerVariable.getExpressionVariable() >= integerVariable.getLowerBoundExpression()); - localSolver->add(integerVariable.getExpressionVariable() <= integerVariable.getUpperBoundExpression()); + localSolver->add(integerVariable.getRangeExpression()); } for (auto const& module : program.getModules()) { for (auto const& integerVariable : module.getIntegerVariables()) { - localSolver->add(integerVariable.getExpressionVariable() >= integerVariable.getLowerBoundExpression()); - localSolver->add(integerVariable.getExpressionVariable() <= integerVariable.getUpperBoundExpression()); + localSolver->add(integerVariable.getRangeExpression()); } } } else {