diff --git a/examples/ets_statem.erl b/examples/ets_statem.erl
index b8527f51..64f4131f 100644
--- a/examples/ets_statem.erl
+++ b/examples/ets_statem.erl
@@ -172,13 +172,15 @@ postcondition(S, {call,_,update_counter,[_Tab, Key, Incr]}, Res) ->
 		     lists:keyfind(Key, 1, S#state.stored)
 	     end,
     Value = element(2, Object),
-    Res =:= Value + Incr;
+    Pred = Res =:= Value + Incr,
+    Msg = "update_counter should return the result of updating the counter.",
+    {Pred, Msg};
 postcondition(_S, {call,_,delete,[_Tab, _Key]}, Res) ->
     Res =:= true;
 postcondition(_S, {call,_,insert,[_Tab, _Object]}, Res) ->
     Res =:= true;
 postcondition(S, {call,_,lookup_element,[_Tab, Key, Pos]}, Res) ->
-    case S#state.type of
+    Pred = case S#state.type of
 	ordered_set ->
 	    Res =:= element(Pos, lists:keyfind(Key, 1, S#state.stored));
 	set ->
@@ -186,7 +188,9 @@ postcondition(S, {call,_,lookup_element,[_Tab, Key, Pos]}, Res) ->
 	_ ->
 	    Res =:= [element(Pos, Tuple)
 		     || Tuple <- proplists:lookup_all(Key, S#state.stored)]
-    end.
+    end,
+    Msg = "lookup_element should return the result of looking up the element",
+    {Pred, Msg}.
 
 
 %%% Sample properties
diff --git a/examples/pdict_statem.erl b/examples/pdict_statem.erl
index bc806e08..d798d23b 100644
--- a/examples/pdict_statem.erl
+++ b/examples/pdict_statem.erl
@@ -20,21 +20,31 @@
 %%% @copyright 2010-2011 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas
 %%% @version {@version}
 %%% @author Kresten Krab Thorup, edited by Eirini Arvaniti
-%%% @doc Simple statem test for the process dictionary
+%%% @doc Simple statem test for a modified API to the process dictionary
 
 -module(pdict_statem).
 -behaviour(proper_statem).
 
+-export([get/1, put/2, erase/1]).
 -export([test/0, test/1]).
 -export([initial_state/0, command/1, precondition/2, postcondition/3,
-	 next_state/3]).
+         next_state/3]).
 
 -include_lib("proper/include/proper.hrl").
 
 -define(KEYS, [a,b,c,d]).
 
+%%% New API in which only get/1 returns an interesting value.
+get(K) -> erlang:get(K).
+put(K,V) ->
+    erlang:put(K,V),
+    ok.
+erase(K) ->
+    erlang:erase(K),
+    ok.
+
 %% A simple statem test for the process dictionary; tests the
-%% operations erlang:put/2, erlang:get/1, erlang:erase/1.
+%% operations ?MODULE:put/2, ?MODULE:get/1, ?MODULE:erase/1.
 
 test() ->
     test(100).
@@ -44,14 +54,17 @@ test(N) ->
 
 prop_pdict() ->
     ?FORALL(Cmds, commands(?MODULE),
-	    begin
-		{H,S,Res} = run_commands(?MODULE, Cmds),
-		clean_up(),
-		?WHENFAIL(
-		   io:format("History: ~w~nState: ~w~nRes: ~w~n",
-			     [H, S, Res]),
-		   aggregate(command_names(Cmds), Res =:= ok))
-	    end).
+            begin
+                {H,S,Res} = run_commands(?MODULE, Cmds),
+                clean_up(),
+                ?WHENFAIL(
+                   begin
+                       {_, _, Msg} = Res,
+                       io:format("History: ~p~nState: ~p~nMsg: ~s~n",
+                                 [H, S, Msg])
+                   end,
+                   aggregate(command_names(Cmds), Res =:= ok))
+            end).
 
 clean_up() ->
     lists:foreach(fun(Key) -> erlang:erase(Key) end, ?KEYS).
@@ -62,41 +75,51 @@ key() ->
 initial_state() -> [].
 
 command([]) ->
-    {call,erlang,put,[key(), integer()]};
+    {call,?MODULE,put,[key(), integer()]};
 command(Props) ->
     ?LET({Key,Value}, weighted_union([{2, elements(Props)},
-				      {1, {key(),integer()}}]),
-	 oneof([{call,erlang,put,[Key,Value]},
-		{call,erlang,get,[Key]},
-		{call,erlang,erase,[Key]}
-	       ])).
+                                      {1, {key(),integer()}}]),
+         oneof([{call,?MODULE,put,[Key,Value]},
+                {call,?MODULE,get,[Key]},
+                {call,?MODULE,erase,[Key]}
+               ])).
 
-precondition(_, {call,erlang,put,[_,_]}) ->
+precondition(_Props, {call,?MODULE,put,[_Key,_Val]}) ->
     true;
-precondition(Props, {call,erlang,get,[Key]}) ->
-    proplists:is_defined(Key, Props);
-precondition(Props, {call,erlang,erase,[Key]}) ->
+precondition(_Props, {call,?MODULE,get,[_Key]}) ->
+    true;
+precondition(Props, {call,?MODULE,erase,[Key]}) ->
     proplists:is_defined(Key, Props);
 precondition(_, _) ->
     false.
 
-postcondition(Props, {call,erlang,put,[Key,_]}, undefined) ->
-    not proplists:is_defined(Key, Props);
-postcondition(Props, {call,erlang,put,[Key,_]}, Old) ->
-    {Key,Old} =:= proplists:lookup(Key, Props);
-postcondition(Props, {call,erlang,get,[Key]}, Val) ->
-    {Key,Val} =:= proplists:lookup(Key, Props);
-postcondition(Props, {call,erlang,erase,[Key]}, Val) ->
-    {Key,Val} =:= proplists:lookup(Key, Props);
+postcondition(_Props, {call,?MODULE,put,[Key,Val]}, Result) ->
+    Want = ok,
+    Pred = (Result =:= Want),
+    Msg = io_lib:format("Want put(~p, ~p) to return ~p, got ~p\n", [Key, Val, Want, Result]),
+    {Pred, Msg};
+postcondition(Props, {call,?MODULE,get,[Key]}, Result) ->
+    Want = case proplists:lookup(Key, Props) of
+                none -> undefined;
+                {Key, Val} -> Val
+           end,
+    Pred = (Result =:= Want),
+    Msg = io_lib:format("Want get(~p) to return ~p, got ~p\n", [Key, Want, Result]),
+    {Pred, Msg};
+postcondition(_Props, {call,?MODULE,erase,[_Key]}, Result) ->
+    Want = ok,
+    Pred = (Result =:= Want),
+    Msg = io_lib:format("Want Result to be ~p, got ~p\n", [Want, Result]),
+    {Pred, Msg};
 postcondition(_, _, _) ->
-    false.
-
-next_state(Props, _Var, {call,erlang,put,[Key,Value]}) ->
-    %% correct model
-    [{Key,Value}|proplists:delete(Key, Props)];
-    %% wrong model
-    %% Props ++ [{Key,Value}];
-next_state(Props, _Var, {call,erlang,erase,[Key]}) ->
-    proplists:delete(Key, Props);
-next_state(Props, _Var, {call,erlang,get,[_]}) ->
+    Msg = "Default case",
+    {false, Msg}.
+
+next_state(Props, _Var, {call,?MODULE,put,[Key,Value]}) ->
+    NewProps = [{Key,Value}|proplists:delete(Key, Props)],
+    NewProps;
+next_state(Props, _Var, {call,?MODULE,erase,[Key]}) ->
+    NewProps = proplists:delete(Key, Props),
+    NewProps;
+next_state(Props, _Var, {call,?MODULE,get,[_]}) ->
     Props.
diff --git a/src/proper.erl b/src/proper.erl
index 454bd804..613d00aa 100644
--- a/src/proper.erl
+++ b/src/proper.erl
@@ -1822,7 +1822,7 @@ print_imm_clean_input({'$conjunction',SubImmCExms}, Prefix, Print) ->
 	end,
     lists:foreach(PrintSubImmCExm, SubImmCExms);
 print_imm_clean_input(Instance, Prefix, Print) ->
-    Print(Prefix ++ "~w~n", [Instance]).
+    Print(Prefix ++ "~s~n", [io_lib_pretty:print(Instance)]).
 
 -spec execute_actions(fail_actions()) -> 'ok'.
 execute_actions(Actions) ->
diff --git a/src/proper_statem.erl b/src/proper_statem.erl
index 815a0e81..15d243a0 100644
--- a/src/proper_statem.erl
+++ b/src/proper_statem.erl
@@ -538,8 +538,13 @@ run_commands(Cmds, Env, Mod, History, State) ->
 				true ->
 				    State2 = proper_symb:eval(Env2, Mod:next_state(State, Res, Call)),
 				    run_commands(Rest, Env2, Mod, History2, State2);
+				{true,_Msg} ->
+				    State2 = proper_symb:eval(Env2, Mod:next_state(State, Res, Call)),
+				    run_commands(Rest, Env2, Mod, History2, State2);
 				false ->
 				    {{lists:reverse(History2), State, {postcondition,false}}, []};
+				{false,Msg} ->
+				    {{lists:reverse(History2), State, {postcondition,false,Msg}}, []};
 				{exception,_,_,_} = Exception ->
 				    {{lists:reverse(History2), State, {postcondition,Exception}}, []}
 			    end;
@@ -563,7 +568,7 @@ check_precondition(Mod, State, Call) ->
     end.
 
 -spec check_postcondition(mod_name(), dynamic_state(), symbolic_call(), term()) ->
-         boolean() | proper:exception().
+         boolean() | {boolean(), string()} | proper:exception().
 check_postcondition(Mod, State, Call, Res) ->
     try Mod:postcondition(State, Call, Res)
     catch