From ec97c53c0b6df3742d3051c061423907cd304e03 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 15 Jul 2015 09:00:41 +0000
Subject: [PATCH] Allow regression test RESULT specifications to refer to
 pre-defined constants in model/properties file too.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10302 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/PrismCL.java | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index 95fa70e5..374ebb30 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -394,8 +394,7 @@ public class PrismCL implements PrismModelListener
 						if (test) {
 							try {
 								mainLog.println();
-								Values allConsts = new Values(definedMFConstants);
-								allConsts.addValues(definedPFConstants);
+								Values allConsts = new Values(modulesFile.getConstantValues(), propertiesFile.getConstantValues());
 								if (propertiesToCheck.get(j).checkAgainstExpectedResult(res.getResult(), allConsts)) {
 									mainLog.println("Testing result: PASS");
 								} else {