diff --git a/prism-tests/functionality/verify/ptas/reach/firewire_abst.nm.props b/prism-tests/functionality/verify/ptas/reach/firewire_abst.nm.props
index 496f78e3..fcb0c480 100644
--- a/prism-tests/functionality/verify/ptas/reach/firewire_abst.nm.props
+++ b/prism-tests/functionality/verify/ptas/reach/firewire_abst.nm.props
@@ -3,7 +3,7 @@
 "eventually": Pmin=? [ F "done" ];
 
 // Minimum probability that a leader has been elected by time T
-// RESULT (delay=30): 0.851563
+// RESULT (delay=30): 0.8515625
 "deadline_min": Pmin=? [ F<=5000 "done" ];
 
 // Maximum probability that a leader has been elected by time T
diff --git a/prism-tests/functionality/verify/ptas/reach/firewire_abst.nm.props.args b/prism-tests/functionality/verify/ptas/reach/firewire_abst.nm.props.args
index 3c9d410c..0edcd016 100644
--- a/prism-tests/functionality/verify/ptas/reach/firewire_abst.nm.props.args
+++ b/prism-tests/functionality/verify/ptas/reach/firewire_abst.nm.props.args
@@ -1,4 +1,5 @@
 -const delay=30 -const L=2 -ptamethod digital
 -const delay=30 -const L=2 -ptamethod digital -ex
+-const delay=30 -const L=2 -ptamethod digital -exact
 -const delay=30 -const L=2 -ptamethod games
 #-const delay=30 -const L=2 -ptamethod backwards
diff --git a/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props b/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props
index 15e77919..0272d15c 100644
--- a/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props
+++ b/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props
@@ -17,6 +17,6 @@ const int T = 150;
 
 // Maximum probability of configuring IP address incorrectly by time T
 // RESULT (T=100): 6.51605e-4
-// RESULT (T=150): 0.00107253
-// RESULT (T=200): 0.00122154
+// RESULT (T=150): 0.001072525539875
+// RESULT (T=200): 0.001221541934004246875
 "deadline": Pmax=? [ F<=T s=2 & ip=2 ];
diff --git a/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props.args b/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props.args
index 80318d38..83880b21 100644
--- a/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props.args
+++ b/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props.args
@@ -1,4 +1,5 @@
 -const L=2 -ptamethod digital -e 1e-8
 -const L=2 -ptamethod digital -e 1e-8 -ex
+-const L=2 -ptamethod digital -exact
 -const L=2 -ptamethod games
 -const L=2 -ptamethod backwards