diff --git a/prism/CHANGELOG.txt b/prism/CHANGELOG.txt
index 7c4c9bbe..eac041e1 100644
--- a/prism/CHANGELOG.txt
+++ b/prism/CHANGELOG.txt
@@ -10,7 +10,7 @@ Ongoing changes:
 * New simulator
 * Adversary generation
 * Access to action labels. inclusion in export, etc.
-* Filters and propert semantics changes/additions
+* Filters and property semantics changes/additions
 
 Latest changes (reverse chronological):
 [correct wrt svn rev 1610]
diff --git a/prism/NOTES b/prism/NOTES
index 6c1371db..bcade9a5 100644
--- a/prism/NOTES
+++ b/prism/NOTES
@@ -1,6 +1,6 @@
 
 Last stable version of PRISM on svn (3.3 plus some fixes) is rev 1405
-(there is a copy of this, e.g. to get working simulator, in ~/prism-old)
+(there is a copy of this, e.g. to get working old simulator, in ~/prism-old)
 
 -----------------------------------------------------------------------
 
@@ -62,6 +62,13 @@ Other notes/ideas:
 -----------------------------------------------------------------------
 
 LTL...
+
+bug:
+
+prism ~/prism-examples/dice/dice.pm \
+-pctl '(s=0|s=1)=>P>=1 [ (P>=0.9 [ F<=1 s=3 ])=>(P>=0.5 [ F<=2 s=4 ]) ]'
+time-bounds should be ok in inner pctl but are not
+
 bscc stuff
 - regression testing on ltl stuff with 3 diff options
 
diff --git a/prism/README.txt b/prism/README.txt
index a74cd3c2..fa0fb4c7 100644
--- a/prism/README.txt
+++ b/prism/README.txt
@@ -91,7 +91,7 @@ Contributions to the development of PRISM have also been gratefully received fro
  * Joachim Meyer-Kayser: Original implementation of the "Fox-Glynn" algorithm
  * Alistair John Strachan: Port to 64-bit architectures
  * Stephen Gilmore: Support for the stochastic process algebra PEPA
- * Paolo Ballarini & Kenneth Chan: Port of PRISM to Mac OS X
+ * Paolo Ballarini & Kenneth Chan: Port to Mac OS X
  * Rashid Mehmood: Improvements to low-level data structures and numerical solution algorithms
  * Alistair John Strachan, Mike Arthur and Zak Cohen: Integration of JFreeChart into PRISM
  * Carlos Bederian (working with Pedro D'Argenio): Addition of LTL model checking for MDPs to PRISM