Browse Source

to be sure: z3model by const reference

tempestpy_adaptions
Sebastian Junges 5 years ago
parent
commit
08cb25c28c
  1. 2
      src/storm/solver/Z3SmtSolver.cpp
  2. 2
      src/storm/solver/Z3SmtSolver.h

2
src/storm/solver/Z3SmtSolver.cpp

@ -7,7 +7,7 @@
namespace storm { namespace storm {
namespace solver { namespace solver {
#ifdef STORM_HAVE_Z3 #ifdef STORM_HAVE_Z3
Z3SmtSolver::Z3ModelReference::Z3ModelReference(storm::expressions::ExpressionManager const& manager, z3::model model, storm::adapters::Z3ExpressionAdapter& expressionAdapter) : ModelReference(manager), model(model), expressionAdapter(expressionAdapter) {
Z3SmtSolver::Z3ModelReference::Z3ModelReference(storm::expressions::ExpressionManager const& manager, z3::model const& model, storm::adapters::Z3ExpressionAdapter& expressionAdapter) : ModelReference(manager), model(model), expressionAdapter(expressionAdapter) {
// Intentionally left empty. // Intentionally left empty.
} }
#endif #endif

2
src/storm/solver/Z3SmtSolver.h

@ -17,7 +17,7 @@ namespace storm {
class Z3ModelReference : public SmtSolver::ModelReference { class Z3ModelReference : public SmtSolver::ModelReference {
public: public:
#ifdef STORM_HAVE_Z3 #ifdef STORM_HAVE_Z3
Z3ModelReference(storm::expressions::ExpressionManager const& manager, z3::model m, storm::adapters::Z3ExpressionAdapter& expressionAdapter);
Z3ModelReference(storm::expressions::ExpressionManager const& manager, z3::model const& m, storm::adapters::Z3ExpressionAdapter& expressionAdapter);
#endif #endif
virtual bool getBooleanValue(storm::expressions::Variable const& variable) const override; virtual bool getBooleanValue(storm::expressions::Variable const& variable) const override;
virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override; virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override;

Loading…
Cancel
Save