From 7af70a77aa51b386926f1630d4a7f3a0e0b8c9f3 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Fri, 14 Sep 2018 17:01:20 +0200 Subject: [PATCH] slight fix to bit vector sizes used in explicit model builder --- src/storm/generator/JaniNextStateGenerator.cpp | 2 +- src/storm/generator/PrismNextStateGenerator.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 62db34455..883abecad 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -185,7 +185,7 @@ namespace storm { std::vector<StateType> initialStateIndices; while (solver->check() == storm::solver::SmtSolver::CheckResult::Sat) { // Create fresh state. - CompressedState initialState(this->variableInformation.getTotalBitOffset()); + CompressedState initialState(this->variableInformation.getTotalBitOffset(true)); // Read variable assignment from the solution of the solver. Also, create an expression we can use to // prevent the variable assignment from being enumerated again. diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 61fe1e80f..9518b2d34 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -150,7 +150,7 @@ namespace storm { std::vector<StateType> initialStateIndices; while (solver->check() == storm::solver::SmtSolver::CheckResult::Sat) { // Create fresh state. - CompressedState initialState(this->variableInformation.getTotalBitOffset()); + CompressedState initialState(this->variableInformation.getTotalBitOffset(true)); // Read variable assignment from the solution of the solver. Also, create an expression we can use to // prevent the variable assignment from being enumerated again.