From 36b38b10ee6eefea6a39b4d90f066da793e2cc81 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 30 May 2017 16:58:24 +0200
Subject: [PATCH] fixed smt minimal command set generator
---
.../counterexamples/SMTMinimalCommandSetGenerator.h | 11 +++++++++++
1 file changed, 11 insertions(+)
diff --git a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h
index dd8602baa..81cff294b 100644
--- a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -1102,6 +1102,10 @@ namespace storm {
static std::vector<storm::expressions::Expression> createCounterCircuit(VariableInformation const& variableInformation, std::vector<storm::expressions::Variable> const& literals) {
STORM_LOG_DEBUG("Creating counter circuit for " << literals.size() << " literals.");
+ if (literals.empty()) {
+ return std::vector<storm::expressions::Expression>();
+ }
+
// Create the auxiliary vector.
std::vector<std::vector<storm::expressions::Expression>> aux;
for (uint_fast64_t index = 0; index < literals.size(); ++index) {
@@ -1143,6 +1147,13 @@ namespace storm {
std::vector<storm::expressions::Variable> const& input = variableInformation.adderVariables;
+ // If there are no input variables, the value is always 0 <= k, so there is nothing to assert.
+ if (input.empty()) {
+ std::stringstream variableName;
+ variableName << "relaxed" << k;
+ return variableInformation.manager->declareBooleanVariable(variableName.str());
+ }
+
storm::expressions::Expression result;
if (bitIsSet(k, 0)) {
result = variableInformation.manager->boolean(true);