......................................................................................................................................................................................................Failed! After 199 tests. [{init,{state,qc_statemc_lets,{state,false,false,undefined,[]}}}, {set,{var,1},{call,qc_leveldb,open,[]}}, {set,{var,2},{call,qc_leveldb,put,[{var,1},{obj,<<"{">>,<<"l\b">>}]}}, {set,{var,3},{call,qc_leveldb,last,[{var,1}]}}, {set,{var,4},{call,qc_leveldb,get,[{var,1},<<"{">>]}}, {set,{var,5},{call,qc_leveldb,close,[{var,1}]}}, {set,{var,6},{call,qc_leveldb,reopen,[]}}, {set,{var,7},{call,qc_leveldb,last,[{var,6}]}}, {set,{var,8},{call,qc_leveldb,next,[{var,6},<<"{">>]}}, {set,{var,9},{call,qc_leveldb,last,[{var,6}]}}, {set,{var,10},{call,qc_leveldb,delete,[{var,6},<<58,108,99,38,4>>]}}, {set,{var,11},{call,qc_leveldb,next,[{var,6},<<>>]}}, {set,{var,12},{call,qc_leveldb,put,[{var,6},{obj,<<"&U">>,<<24,116,1>>}]}}, {set,{var,13},{call,qc_leveldb,next,[{var,6},<<"s\t">>]}}, {set,{var,14}, {call,qc_leveldb,put,[{var,6},{obj,<<17,11,41>>,<<26,65,39,56>>}]}}, {set,{var,15},{call,qc_leveldb,last,[{var,6}]}}, {set,{var,16},{call,qc_leveldb,next,[{var,6},<<"[vn">>]}}, {set,{var,17},{call,qc_leveldb,last,[{var,6}]}}, {set,{var,18},{call,qc_leveldb,put,[{var,6},{obj,<<"&U">>,<<24,116,1>>}]}}, {set,{var,19}, {call,qc_leveldb,put,[{var,6},{obj,<<17,11,41>>,<<26,65,39,56>>}]}}, {set,{var,20},{call,qc_leveldb,close,[{var,6}]}}, {set,{var,21},{call,qc_leveldb,reopen,[]}}, {set,{var,22},{call,qc_leveldb,last,[{var,21}]}}, {set,{var,23},{call,qc_leveldb,last,[{var,21}]}}, {set,{var,24},{call,qc_leveldb,get,[{var,21},<<"{">>]}}, {set,{var,25},{call,qc_leveldb,put,[{var,21},{obj,<<"0%E0>,<<>>}]}}, {set,{var,26},{call,qc_leveldb,next,[{var,21},<<"0%E0>]}}, {set,{var,27},{call,qc_leveldb,delete,[{var,21},<<17,11,41>>]}}, {set,{var,28},{call,qc_leveldb,last,[{var,21}]}}, {set,{var,29},{call,qc_leveldb,close,[{var,21}]}}, {set,{var,30},{call,qc_leveldb,reopen,[]}}, {set,{var,31},{call,qc_leveldb,get,[{var,30},<<"!">>]}}, {set,{var,32},{call,qc_leveldb,next,[{var,30},<<"0%E0>]}}, {set,{var,33},{call,qc_leveldb,get,[{var,30},<<"G">>]}}, {set,{var,34},{call,qc_leveldb,delete,[{var,30},<<"&U">>]}}, {set,{var,35},{call,qc_leveldb,delete,[{var,30},<<"{">>]}}, {set,{var,36},{call,qc_leveldb,get,[{var,30},<<>>]}}, {set,{var,37},{call,qc_leveldb,first,[{var,30}]}}, {set,{var,38},{call,qc_leveldb,put,[{var,30},{obj,<<"0%E0>,<<>>}]}}, {set,{var,39},{call,qc_leveldb,delete,[{var,30},<<"0%E0>]}}, {set,{var,40},{call,qc_leveldb,close,[{var,30}]}}, {set,{var,41},{call,qc_leveldb,reopen,[]}}, {set,{var,42},{call,qc_leveldb,next,[{var,41},<<1,100>>]}}, {set,{var,43},{call,qc_leveldb,delete,[{var,41},<<105,83,0>>]}}, {set,{var,44},{call,qc_leveldb,next,[{var,41},<<57,22,110>>]}}, {set,{var,45}, {call,qc_leveldb,put,[{var,41},{obj,<<86,111,5,117>>,<<"ke~@g">>}]}}, {set,{var,46},{call,qc_leveldb,close,[{var,41}]}}, {set,{var,47},{call,qc_leveldb,reopen,[]}}, {set,{var,48},{call,qc_leveldb,next,[{var,47},<<86,111,5,117>>]}}, {set,{var,49},{call,qc_leveldb,last,[{var,47}]}}, {set,{var,50},{call,qc_leveldb,put,[{var,47},{obj,<<"?y">>,<<"=1~">>}]}}, {set,{var,51}, {call,qc_leveldb,put,[{var,47},{obj,<<86,111,5,117>>,<<"ke~@g">>}]}}, {set,{var,52},{call,qc_leveldb,next,[{var,47},<<"?y">>]}}, {set,{var,53},{call,qc_leveldb,last,[{var,47}]}}, {set,{var,54},{call,qc_leveldb,get,[{var,47},<<"H\\">>]}}, {set,{var,55},{call,qc_leveldb,delete,[{var,47},<<84,22,83>>]}}, {set,{var,56},{call,qc_leveldb,delete,[{var,47},<<"\f=b">>]}}, {set,{var,57},{call,qc_leveldb,first,[{var,47}]}}, {set,{var,58},{call,qc_leveldb,put,[{var,47},{obj,<<"k">>,<<"g?">>}]}}, {set,{var,59},{call,qc_leveldb,next,[{var,47},<<"{">>]}}, {set,{var,60},{call,qc_leveldb,get,[{var,47},<<"yE">>]}}, {set,{var,61},{call,qc_leveldb,next,[{var,47},<<"?y">>]}}, {set,{var,62},{call,qc_leveldb,last,[{var,47}]}}, {set,{var,63},{call,qc_leveldb,next,[{var,47},<<"A">>]}}, {set,{var,64},{call,qc_leveldb,put,[{var,47},{obj,<<>>,<<"57QmN">>}]}}, {set,{var,65}, {call,qc_leveldb,put,[{var,47},{obj,<<"NN\tt6">>,<<26,89,8>>}]}}, {set,{var,66},{call,qc_leveldb,delete,[{var,47},<<>>]}}, {set,{var,67},{call,qc_leveldb,next,[{var,47},<<117,42,14>>]}}, {set,{var,68},{call,qc_leveldb,next,[{var,47},<<"?y">>]}}] COMMANDS: "qc_statem-20111005-175140.erl" HISTORY: #1: Cmd: {set,{var,1},{call,qc_leveldb,open,[]}} Reply: {ptr,{struct,leveldb_t},4435483200} State: {state,qc_statemc_lets,{state,false,false,undefined,[]}} #2: Cmd: {set,{var,2}, {call,qc_leveldb,put,[{var,1},{obj,<<"{">>,<<"l\b">>}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435483200}, []}} #3: Cmd: {set,{var,3},{call,qc_leveldb,last,[{var,1}]}} Reply: <<"{">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435483200}, [{obj,<<"{">>,<<"l\b">>}]}} #4: Cmd: {set,{var,4},{call,qc_leveldb,get,[{var,1},<<"{">>]}} Reply: <<"l\b">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435483200}, [{obj,<<"{">>,<<"l\b">>}]}} #5: Cmd: {set,{var,5},{call,qc_leveldb,close,[{var,1}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435483200}, [{obj,<<"{">>,<<"l\b">>}]}} #6: Cmd: {set,{var,6},{call,qc_leveldb,reopen,[]}} Reply: {ptr,{struct,leveldb_t},4435481968} State: {state,qc_statemc_lets, {state,false,true,undefined,[{obj,<<"{">>,<<"l\b">>}]}} #7: Cmd: {set,{var,7},{call,qc_leveldb,last,[{var,6}]}} Reply: <<"{">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435481968}, [{obj,<<"{">>,<<"l\b">>}]}} #8: Cmd: {set,{var,8},{call,qc_leveldb,next,[{var,6},<<"{">>]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435481968}, [{obj,<<"{">>,<<"l\b">>}]}} #9: Cmd: {set,{var,9},{call,qc_leveldb,last,[{var,6}]}} Reply: <<"{">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435481968}, [{obj,<<"{">>,<<"l\b">>}]}} #10: Cmd: {set,{var,10}, {call,qc_leveldb,delete,[{var,6},<<58,108,99,38,4>>]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435481968}, [{obj,<<"{">>,<<"l\b">>}]}} #11: Cmd: {set,{var,11},{call,qc_leveldb,next,[{var,6},<<>>]}} Reply: <<"{">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435481968}, [{obj,<<"{">>,<<"l\b">>}]}} #12: Cmd: {set,{var,12}, {call,qc_leveldb,put,[{var,6},{obj,<<"&U">>,<<24,116,1>>}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435481968}, [{obj,<<"{">>,<<"l\b">>}]}} #13: Cmd: {set,{var,13},{call,qc_leveldb,next,[{var,6},<<"s\t">>]}} Reply: <<"{">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435481968}, [{obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #14: Cmd: {set,{var,14}, {call,qc_leveldb,put, [{var,6},{obj,<<17,11,41>>,<<26,65,39,56>>}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435481968}, [{obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #15: Cmd: {set,{var,15},{call,qc_leveldb,last,[{var,6}]}} Reply: <<"{">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435481968}, [{obj,<<17,11,41>>,<<26,65,39,56>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #16: Cmd: {set,{var,16},{call,qc_leveldb,next,[{var,6},<<"[vn">>]}} Reply: <<"{">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435481968}, [{obj,<<17,11,41>>,<<26,65,39,56>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #17: Cmd: {set,{var,17},{call,qc_leveldb,last,[{var,6}]}} Reply: <<"{">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435481968}, [{obj,<<17,11,41>>,<<26,65,39,56>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #18: Cmd: {set,{var,18}, {call,qc_leveldb,put,[{var,6},{obj,<<"&U">>,<<24,116,1>>}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435481968}, [{obj,<<17,11,41>>,<<26,65,39,56>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #19: Cmd: {set,{var,19}, {call,qc_leveldb,put, [{var,6},{obj,<<17,11,41>>,<<26,65,39,56>>}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435481968}, [{obj,<<17,11,41>>,<<26,65,39,56>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #20: Cmd: {set,{var,20},{call,qc_leveldb,close,[{var,6}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435481968}, [{obj,<<17,11,41>>,<<26,65,39,56>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #21: Cmd: {set,{var,21},{call,qc_leveldb,reopen,[]}} Reply: {ptr,{struct,leveldb_t},4435480304} State: {state,qc_statemc_lets, {state,false,true,undefined, [{obj,<<17,11,41>>,<<26,65,39,56>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #22: Cmd: {set,{var,22},{call,qc_leveldb,last,[{var,21}]}} Reply: <<"{">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480304}, [{obj,<<17,11,41>>,<<26,65,39,56>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #23: Cmd: {set,{var,23},{call,qc_leveldb,last,[{var,21}]}} Reply: <<"{">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480304}, [{obj,<<17,11,41>>,<<26,65,39,56>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #24: Cmd: {set,{var,24},{call,qc_leveldb,get,[{var,21},<<"{">>]}} Reply: <<"l\b">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480304}, [{obj,<<17,11,41>>,<<26,65,39,56>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #25: Cmd: {set,{var,25}, {call,qc_leveldb,put,[{var,21},{obj,<<"0%E0>,<<>>}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480304}, [{obj,<<17,11,41>>,<<26,65,39,56>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #26: Cmd: {set,{var,26},{call,qc_leveldb,next,[{var,21},<<"0%E0>]}} Reply: <<"{">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480304}, [{obj,<<"0%E0>,<<>>}, {obj,<<17,11,41>>,<<26,65,39,56>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #27: Cmd: {set,{var,27},{call,qc_leveldb,delete,[{var,21},<<17,11,41>>]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480304}, [{obj,<<"0%E0>,<<>>}, {obj,<<17,11,41>>,<<26,65,39,56>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #28: Cmd: {set,{var,28},{call,qc_leveldb,last,[{var,21}]}} Reply: <<"{">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480304}, [{obj,<<"0%E0>,<<>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #29: Cmd: {set,{var,29},{call,qc_leveldb,close,[{var,21}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480304}, [{obj,<<"0%E0>,<<>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #30: Cmd: {set,{var,30},{call,qc_leveldb,reopen,[]}} Reply: {ptr,{struct,leveldb_t},4435480288} State: {state,qc_statemc_lets, {state,false,true,undefined, [{obj,<<"0%E0>,<<>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #31: Cmd: {set,{var,31},{call,qc_leveldb,get,[{var,30},<<"!">>]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480288}, [{obj,<<"0%E0>,<<>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #32: Cmd: {set,{var,32},{call,qc_leveldb,next,[{var,30},<<"0%E0>]}} Reply: <<"{">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480288}, [{obj,<<"0%E0>,<<>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #33: Cmd: {set,{var,33},{call,qc_leveldb,get,[{var,30},<<"G">>]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480288}, [{obj,<<"0%E0>,<<>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #34: Cmd: {set,{var,34},{call,qc_leveldb,delete,[{var,30},<<"&U">>]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480288}, [{obj,<<"0%E0>,<<>>}, {obj,<<"&U">>,<<24,116,1>>}, {obj,<<"{">>,<<"l\b">>}]}} #35: Cmd: {set,{var,35},{call,qc_leveldb,delete,[{var,30},<<"{">>]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480288}, [{obj,<<"0%E0>,<<>>}, {obj,<<"{">>,<<"l\b">>}]}} #36: Cmd: {set,{var,36},{call,qc_leveldb,get,[{var,30},<<>>]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480288}, [{obj,<<"0%E0>,<<>>}]}} #37: Cmd: {set,{var,37},{call,qc_leveldb,first,[{var,30}]}} Reply: <<"0%E0> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480288}, [{obj,<<"0%E0>,<<>>}]}} #38: Cmd: {set,{var,38}, {call,qc_leveldb,put,[{var,30},{obj,<<"0%E0>,<<>>}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480288}, [{obj,<<"0%E0>,<<>>}]}} #39: Cmd: {set,{var,39},{call,qc_leveldb,delete,[{var,30},<<"0%E0>]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480288}, [{obj,<<"0%E0>,<<>>}]}} #40: Cmd: {set,{var,40},{call,qc_leveldb,close,[{var,30}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435480288}, []}} #41: Cmd: {set,{var,41},{call,qc_leveldb,reopen,[]}} Reply: {ptr,{struct,leveldb_t},4435483152} State: {state,qc_statemc_lets,{state,false,true,undefined,[]}} #42: Cmd: {set,{var,42},{call,qc_leveldb,next,[{var,41},<<1,100>>]}} Reply: <<"{">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4435483152}, []}} RESULT: {postcondition,<<"{">>} STATE: {state,qc_statemc_lets, {state,false,true,{ptr,{struct,leveldb_t},4435483152},[]}} STATE IS SANE: true Shrinking.............................(29 times) [{init,{state,qc_statemc_lets,{state,false,false,undefined,[]}}}, {set,{var,1},{call,qc_leveldb,open,[]}}, {set,{var,2},{call,qc_leveldb,put,[{var,1},{obj,<<"{">>,<<>>}]}}, {set,{var,5},{call,qc_leveldb,close,[{var,1}]}}, {set,{var,6},{call,qc_leveldb,reopen,[]}}, {set,{var,10},{call,qc_leveldb,delete,[{var,6},<<18>>]}}, {set,{var,20},{call,qc_leveldb,close,[{var,6}]}}, {set,{var,21},{call,qc_leveldb,reopen,[]}}, {set,{var,25},{call,qc_leveldb,put,[{var,21},{obj,<<"0%E0>,<<>>}]}}, {set,{var,27},{call,qc_leveldb,delete,[{var,21},<<17,11,41>>]}}, {set,{var,29},{call,qc_leveldb,close,[{var,21}]}}, {set,{var,30},{call,qc_leveldb,reopen,[]}}, {set,{var,35},{call,qc_leveldb,delete,[{var,30},<<"{">>]}}, {set,{var,39},{call,qc_leveldb,delete,[{var,30},<<"0%E0>]}}, {set,{var,40},{call,qc_leveldb,close,[{var,30}]}}, {set,{var,41},{call,qc_leveldb,reopen,[]}}, {set,{var,42},{call,qc_leveldb,next,[{var,41},<<>>]}}] COMMANDS: "qc_statem-20111005-180302.erl" HISTORY: #1: Cmd: {set,{var,1},{call,qc_leveldb,open,[]}} Reply: {ptr,{struct,leveldb_t},4465891904} State: {state,qc_statemc_lets,{state,false,false,undefined,[]}} #2: Cmd: {set,{var,2},{call,qc_leveldb,put,[{var,1},{obj,<<"{">>,<<>>}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4465891904}, []}} #3: Cmd: {set,{var,5},{call,qc_leveldb,close,[{var,1}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4465891904}, [{obj,<<"{">>,<<>>}]}} #4: Cmd: {set,{var,6},{call,qc_leveldb,reopen,[]}} Reply: {ptr,{struct,leveldb_t},4465890576} State: {state,qc_statemc_lets, {state,false,true,undefined,[{obj,<<"{">>,<<>>}]}} #5: Cmd: {set,{var,10},{call,qc_leveldb,delete,[{var,6},<<18>>]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4465890576}, [{obj,<<"{">>,<<>>}]}} #6: Cmd: {set,{var,20},{call,qc_leveldb,close,[{var,6}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4465890576}, [{obj,<<"{">>,<<>>}]}} #7: Cmd: {set,{var,21},{call,qc_leveldb,reopen,[]}} Reply: {ptr,{struct,leveldb_t},4465890448} State: {state,qc_statemc_lets, {state,false,true,undefined,[{obj,<<"{">>,<<>>}]}} #8: Cmd: {set,{var,25}, {call,qc_leveldb,put,[{var,21},{obj,<<"0%E0>,<<>>}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4465890448}, [{obj,<<"{">>,<<>>}]}} #9: Cmd: {set,{var,27},{call,qc_leveldb,delete,[{var,21},<<17,11,41>>]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4465890448}, [{obj,<<"0%E0>,<<>>},{obj,<<"{">>,<<>>}]}} #10: Cmd: {set,{var,29},{call,qc_leveldb,close,[{var,21}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4465890448}, [{obj,<<"0%E0>,<<>>},{obj,<<"{">>,<<>>}]}} #11: Cmd: {set,{var,30},{call,qc_leveldb,reopen,[]}} Reply: {ptr,{struct,leveldb_t},4465892480} State: {state,qc_statemc_lets, {state,false,true,undefined, [{obj,<<"0%E0>,<<>>},{obj,<<"{">>,<<>>}]}} #12: Cmd: {set,{var,35},{call,qc_leveldb,delete,[{var,30},<<"{">>]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4465892480}, [{obj,<<"0%E0>,<<>>},{obj,<<"{">>,<<>>}]}} #13: Cmd: {set,{var,39},{call,qc_leveldb,delete,[{var,30},<<"0%E0>]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4465892480}, [{obj,<<"0%E0>,<<>>}]}} #14: Cmd: {set,{var,40},{call,qc_leveldb,close,[{var,30}]}} Reply: true State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4465892480}, []}} #15: Cmd: {set,{var,41},{call,qc_leveldb,reopen,[]}} Reply: {ptr,{struct,leveldb_t},4465889136} State: {state,qc_statemc_lets,{state,false,true,undefined,[]}} #16: Cmd: {set,{var,42},{call,qc_leveldb,next,[{var,41},<<>>]}} Reply: <<"{">> State: {state,qc_statemc_lets, {state,false,true, {ptr,{struct,leveldb_t},4465889136}, []}} RESULT: {postcondition,<<"{">>} STATE: {state,qc_statemc_lets, {state,false,true,{ptr,{struct,leveldb_t},4465889136},[]}} STATE IS SANE: true false 2>