diff --git a/README.md b/README.md
index 83d6714..a72224d 100644
--- a/README.md
+++ b/README.md
@@ -101,9 +101,7 @@ supported APIs are:</p>
 <p><em>This repository is experimental in nature - use at your own risk and
 please contribute if you find LETS useful.</em></p>
 
-
-##Quick Start Recipe##
-
+<h2 id="_quick_start_recipe">Quick Start Recipe</h2>
 
 <p>To download and build the lets application in one shot, please follow
 this recipe:</p>
@@ -124,7 +122,7 @@ please read further.</p>
 
 
 
-##Documentation##
+<h2 id="_documentation">Documentation</h2>
 
 
 <h3 id="_where_should_i_start">Where should I start?</h3>
@@ -134,12 +132,16 @@ please read further.</p>
 specification and behavior of ETS and LETS.  These QC tests also
 illustrate several strategies for testing Erlang Driver-based and
 NIF-based implementations.</p>
+
+
 <h3 id="_what_is_ets_and_dets">What is ETS and DETS?</h3>
 <p>ETS and DETS are Erlang/OTP's standard library modules for Erlang
 term storage.  ETS is a memory-based implementation.  DETS is a
 disk-based implementation.</p>
 <p>See <a href="http://www.erlang.org/doc/man/ets.html">http://www.erlang.org/doc/man/ets.html</a> and
 <a href="http://www.erlang.org/doc/man/dets.html">http://www.erlang.org/doc/man/dets.html</a> for further details.</p>
+
+
 <h3 id="_what_is_leveldb">What is LevelDB?</h3>
 <p>LevelDB is a fast key-value storage library written at Google that
 provides an ordered mapping from string keys to string values.</p>
@@ -147,8 +149,8 @@ provides an ordered mapping from string keys to string values.</p>
 
 
 
-##To download##
 
+<h2 id="_to_download">To download</h2>
 
 <ol class="arabic">
 <li>
@@ -293,8 +295,7 @@ Repo - <a href="http://source.android.com/source/git-repo.md">http://source.andr
 
 
 
-##To build - basic recipe##
-
+<h2 id="_to_build_basic_recipe">To build - basic recipe</h2>
 
 <ol class="arabic">
 <li>
@@ -316,8 +317,7 @@ $ make compile</tt></pre>
 
 
 
-##To build - optional features##
-
+<h2 id="_to_build_optional_features">To build - optional features</h2>
 
 <ol class="upperalpha">
 <li>
@@ -381,8 +381,7 @@ $ make dialyze-nospec</tt></pre>
 
 
 
-##To test - QuickCheck##
-
+<h2 id="_to_test_quickcheck">To test - QuickCheck</h2>
 
 <ol class="arabic">
 <li>
@@ -433,8 +432,7 @@ Tip
 
 
 
-##To test - Proper##
-
+<h2 id="_to_test_proper">To test - Proper</h2>
 
 <ol class="arabic">
 <li>
@@ -476,8 +474,7 @@ $ erl -smp +A 5 -pz ../../sext/ebin -pz ../../qc/ebin
 
 
 
-##Roadmap##
-
+<h2 id="_roadmap">Roadmap</h2>
 
 <ul>
 <li>
@@ -501,22 +498,6 @@ Explain how to build and to run lets with valgrind enabled
 </li>
 <li>
 <p>
-Bugs
-</p>
-<ul>
-<li>
-<p>
-LevelDB - Reappearing "ghost" key after 17 steps
-    (<a href="http://code.google.com/p/leveldb/issues/detail?id=44">http://code.google.com/p/leveldb/issues/detail?id=44</a>)
-   <br>
-    NOTE: LET's QC tests are hard-coded not to close and then to
-    reopen a LevelDB database until this bug has been fixed.
-</p>
-</li>
-</ul>
-</li>
-<li>
-<p>
 Performance
 </p>
 <ul>
diff --git a/doc/README.md b/doc/README.md
index 915d346..ec85905 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -101,9 +101,7 @@ supported APIs are:</p>
 <p><em>This repository is experimental in nature - use at your own risk and
 please contribute if you find LETS useful.</em></p>
 
-
-##Quick Start Recipe##
-
+<h2 id="_quick_start_recipe">Quick Start Recipe</h2>
 
 <p>To download and build the lets application in one shot, please follow
 this recipe:</p>
@@ -124,7 +122,7 @@ please read further.</p>
 
 
 
-##Documentation##
+<h2 id="_documentation">Documentation</h2>
 
 
 <h3 id="_where_should_i_start">Where should I start?</h3>
@@ -134,12 +132,16 @@ please read further.</p>
 specification and behavior of ETS and LETS.  These QC tests also
 illustrate several strategies for testing Erlang Driver-based and
 NIF-based implementations.</p>
+
+
 <h3 id="_what_is_ets_and_dets">What is ETS and DETS?</h3>
 <p>ETS and DETS are Erlang/OTP's standard library modules for Erlang
 term storage.  ETS is a memory-based implementation.  DETS is a
 disk-based implementation.</p>
 <p>See <a href="http://www.erlang.org/doc/man/ets.html">http://www.erlang.org/doc/man/ets.html</a> and
 <a href="http://www.erlang.org/doc/man/dets.html">http://www.erlang.org/doc/man/dets.html</a> for further details.</p>
+
+
 <h3 id="_what_is_leveldb">What is LevelDB?</h3>
 <p>LevelDB is a fast key-value storage library written at Google that
 provides an ordered mapping from string keys to string values.</p>
@@ -147,8 +149,8 @@ provides an ordered mapping from string keys to string values.</p>
 
 
 
-##To download##
 
+<h2 id="_to_download">To download</h2>
 
 <ol class="arabic">
 <li>
@@ -293,8 +295,7 @@ Repo - <a href="http://source.android.com/source/git-repo.md">http://source.andr
 
 
 
-##To build - basic recipe##
-
+<h2 id="_to_build_basic_recipe">To build - basic recipe</h2>
 
 <ol class="arabic">
 <li>
@@ -316,8 +317,7 @@ $ make compile</tt></pre>
 
 
 
-##To build - optional features##
-
+<h2 id="_to_build_optional_features">To build - optional features</h2>
 
 <ol class="upperalpha">
 <li>
@@ -381,8 +381,7 @@ $ make dialyze-nospec</tt></pre>
 
 
 
-##To test - QuickCheck##
-
+<h2 id="_to_test_quickcheck">To test - QuickCheck</h2>
 
 <ol class="arabic">
 <li>
@@ -433,8 +432,7 @@ Tip
 
 
 
-##To test - Proper##
-
+<h2 id="_to_test_proper">To test - Proper</h2>
 
 <ol class="arabic">
 <li>
@@ -476,8 +474,7 @@ $ erl -smp +A 5 -pz ../../sext/ebin -pz ../../qc/ebin
 
 
 
-##Roadmap##
-
+<h2 id="_roadmap">Roadmap</h2>
 
 <ul>
 <li>
@@ -501,22 +498,6 @@ Explain how to build and to run lets with valgrind enabled
 </li>
 <li>
 <p>
-Bugs
-</p>
-<ul>
-<li>
-<p>
-LevelDB - Reappearing "ghost" key after 17 steps
-    (<a href="http://code.google.com/p/leveldb/issues/detail?id=44">http://code.google.com/p/leveldb/issues/detail?id=44</a>)
-   <br>
-    NOTE: LET's QC tests are hard-coded not to close and then to
-    reopen a LevelDB database until this bug has been fixed.
-</p>
-</li>
-</ul>
-</li>
-<li>
-<p>
 Performance
 </p>
 <ul>
@@ -620,6 +601,7 @@ consider adding explicit read_options and write_options for LET's
 
 
 
+
 ##Modules##
 
 
diff --git a/doc/overview.edoc b/doc/overview.edoc
index a707699..e85f426 100644
--- a/doc/overview.edoc
+++ b/doc/overview.edoc
@@ -255,13 +255,6 @@ $ erl -smp +A 5 -pz ../../sext/ebin -pz ../../qc/ebin
   * Explain how to build and to run lets with valgrind enabled
     OTP/Erlang virtual machine
 
-- Bugs
-  * LevelDB - Reappearing "ghost" key after 17 steps
-    (http://code.google.com/p/leveldb/issues/detail?id=44)
-    +
-    NOTE: LET\'s QC tests are hard-coded not to close and then to
-    reopen a LevelDB database until this bug has been fixed.
-
 - Performance
   * Update driver implementation to use Erlang\'s asynchronous driver
     thread pool for all LevelDB operations.
diff --git a/priv/test/.gitignore b/priv/test/.gitignore
new file mode 100644
index 0000000..37f19b5
--- /dev/null
+++ b/priv/test/.gitignore
@@ -0,0 +1,3 @@
+*.o
+qc_leveldb_issue44
+qc_leveldb/
diff --git a/priv/test/Makefile b/priv/test/Makefile
new file mode 100644
index 0000000..4f1332e
--- /dev/null
+++ b/priv/test/Makefile
@@ -0,0 +1,26 @@
+
+LEVELDB_DIR=../../c_src/leveldb
+SNAPPY_DIR=../../c_src/snappy
+
+CC=gcc
+CFLAGS=-Wall -I $(LEVELDB_DIR)/include
+LDFLAGS=$(LEVELDB_DIR)/lib/libleveldb.a $(SNAPPY_DIR)/lib/libsnappy.a -lstdc++ -lpthread
+
+TEST=qc_leveldb_issue44
+
+HEADERS=qc_statemc_lets.h
+SOURCES=qc_statemc_lets.c $(TEST:=.c)
+OBJECTS=$(SOURCES:.c=.o)
+
+.PHONY: clean
+
+all: $(SOURCES) $(TEST)
+
+$(TEST): $(OBJECTS) $(HEADERS)
+	$(CC) $(OBJECTS) $(LDFLAGS) -o $@
+
+.c.o:
+	$(CC) -c $(CFLAGS) $< -o $@
+
+clean:
+	rm -rf *.o $(EXECUTABLE) qc_leveldb
diff --git a/priv/test/qc_leveldb_issue44.c b/priv/test/qc_leveldb_issue44.c
new file mode 100644
index 0000000..5d8bbcf
--- /dev/null
+++ b/priv/test/qc_leveldb_issue44.c
@@ -0,0 +1,280 @@
+// %%% The MIT License
+// %%%
+// %%% Copyright (C) 2011 by Joseph Wayne Norton <norton@alum.mit.edu>
+// %%%
+// %%% Permission is hereby granted, free of charge, to any person obtaining a copy
+// %%% of this software and associated documentation files (the "Software"), to deal
+// %%% in the Software without restriction, including without limitation the rights
+// %%% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+// %%% copies of the Software, and to permit persons to whom the Software is
+// %%% furnished to do so, subject to the following conditions:
+// %%%
+// %%% The above copyright notice and this permission notice shall be included in
+// %%% all copies or substantial portions of the Software.
+// %%%
+// %%% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+// %%% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+// %%% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+// %%% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+// %%% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+// %%% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+// %%% THE SOFTWARE.
+
+#include <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <unistd.h>
+
+#include "qc_statemc_lets.h"
+
+
+int main() {
+    leveldb_t* Db;
+    char g[1] = {'g'};
+    size_t glen = 1;
+    char nil[0] = {};
+    size_t nillen = 0;
+
+    // #1
+    Db = open0();
+
+    // #2
+    close1(Db);
+
+    // #3
+    Db = reopen0();
+
+    // #4
+    put2(Db, g, glen, nil, nillen);
+
+    // #5
+    close1(Db);
+
+    // #6
+    Db = reopen0();
+
+    // #7
+    delete2(Db, g, glen);
+
+    // #8
+    delete2(Db, nil, nillen);
+
+    // #9
+    close1(Db);
+
+    // #10
+    Db = reopen0();
+
+    // #11
+    delete2(Db, nil, nillen);
+
+    // #12
+    close1(Db);
+
+    // #13
+    Db = reopen0();
+
+    // #14
+    put2(Db, nil, nillen, nil, nillen);
+
+    // #15
+    close1(Db);
+
+    // #16
+    Db = reopen0();
+
+    // #17
+    close1(Db);
+
+    // #18
+    Db = reopen0();
+
+    // #19a
+    char* bug = NULL;
+    size_t buglen = 0;
+    bug = last1(Db, &buglen);
+
+    if (buglen == nillen && memcmp(bug, nil, nillen) == 0) {
+        fprintf(stderr, "\n\n!!! NO - reappearing ghost key 'g' !!!\n\n");
+    }
+    assert(buglen == nillen);
+    assert(memcmp(bug, nil, nillen) == 0);
+
+    fprintf(stderr, "KEY POINT => sleep for background compaction to finish it's work");
+    sleep(1);
+
+    // #19a
+    bug = NULL;
+    buglen = 0;
+    bug = last1(Db, &buglen);
+
+    if (buglen == glen && memcmp(bug, g, glen) == 0) {
+        fprintf(stderr, "\n\n!!! YES - reappearing ghost key 'g' !!!\n\n");
+    }
+    assert(buglen == nillen);
+    assert(memcmp(bug, nil, nillen) == 0);
+
+    return 0;
+}
+
+/*
+Failed!
+[{init,{state,qc_statemc_lets,{state,false,false,undefined,[]}}},
+ {set,{var,1},{call,qc_leveldb,open,[]}},
+ {set,{var,4},{call,qc_leveldb,close,[{var,1}]}},
+ {set,{var,5},{call,qc_leveldb,reopen,[]}},
+ {set,{var,6},{call,qc_leveldb,put,[{var,5},{obj,<<"a">>,<<>>}]}},
+ {set,{var,9},{call,qc_leveldb,close,[{var,5}]}},
+ {set,{var,10},{call,qc_leveldb,reopen,[]}},
+ {set,{var,11},{call,qc_leveldb,delete,[{var,10},<<"a">>]}},
+ {set,{var,14},{call,qc_leveldb,delete,[{var,10},<<>>]}},
+ {set,{var,15},{call,qc_leveldb,close,[{var,10}]}},
+ {set,{var,19},{call,qc_leveldb,reopen,[]}},
+ {set,{var,22},{call,qc_leveldb,delete,[{var,19},<<>>]}},
+ {set,{var,26},{call,qc_leveldb,close,[{var,19}]}},
+ {set,{var,27},{call,qc_leveldb,reopen,[]}},
+ {set,{var,31},{call,qc_leveldb,put,[{var,27},{obj,<<>>,<<>>}]}},
+ {set,{var,33},{call,qc_leveldb,close,[{var,27}]}},
+ {set,{var,34},{call,qc_leveldb,reopen,[]}},
+ {set,{var,36},{call,qc_leveldb,close,[{var,34}]}},
+ {set,{var,37},{call,qc_leveldb,reopen,[]}},
+ {set,{var,40},{call,qc_leveldb,last,[{var,37}]}}]
+
+COMMANDS:
+        "qc_statem-20111029-191936.erl"
+
+HISTORY:
+ #1:
+        Cmd: {set,{var,1},{call,qc_leveldb,open,[]}}
+        Reply: {ptr,{struct,leveldb_t},16833504}
+        State: {state,qc_statemc_lets,{state,false,false,undefined,[]}}
+
+ #2:
+        Cmd: {set,{var,4},{call,qc_leveldb,close,[{var,1}]}}
+        Reply: true
+        State: {state,qc_statemc_lets,
+                      {state,false,true,{ptr,{struct,leveldb_t},16833504},[]}}
+
+ #3:
+        Cmd: {set,{var,5},{call,qc_leveldb,reopen,[]}}
+        Reply: {ptr,{struct,leveldb_t},16833616}
+        State: {state,qc_statemc_lets,{state,false,true,undefined,[]}}
+
+ #4:
+        Cmd: {set,{var,6},{call,qc_leveldb,put,[{var,5},{obj,<<"a">>,<<>>}]}}
+        Reply: true
+        State: {state,qc_statemc_lets,
+                      {state,false,true,{ptr,{struct,leveldb_t},16833616},[]}}
+
+ #5:
+        Cmd: {set,{var,9},{call,qc_leveldb,close,[{var,5}]}}
+        Reply: true
+        State: {state,qc_statemc_lets,
+                      {state,false,true,
+                             {ptr,{struct,leveldb_t},16833616},
+                             [{obj,<<"a">>,<<>>}]}}
+
+ #6:
+        Cmd: {set,{var,10},{call,qc_leveldb,reopen,[]}}
+        Reply: {ptr,{struct,leveldb_t},16831264}
+        State: {state,qc_statemc_lets,
+                      {state,false,true,undefined,[{obj,<<"a">>,<<>>}]}}
+
+ #7:
+        Cmd: {set,{var,11},{call,qc_leveldb,delete,[{var,10},<<"a">>]}}
+        Reply: true
+        State: {state,qc_statemc_lets,
+                      {state,false,true,
+                             {ptr,{struct,leveldb_t},16831264},
+                             [{obj,<<"a">>,<<>>}]}}
+
+ #8:
+        Cmd: {set,{var,14},{call,qc_leveldb,delete,[{var,10},<<>>]}}
+        Reply: true
+        State: {state,qc_statemc_lets,
+                      {state,false,true,{ptr,{struct,leveldb_t},16831264},[]}}
+
+ #9:
+        Cmd: {set,{var,15},{call,qc_leveldb,close,[{var,10}]}}
+        Reply: true
+        State: {state,qc_statemc_lets,
+                      {state,false,true,{ptr,{struct,leveldb_t},16831264},[]}}
+
+ #10:
+        Cmd: {set,{var,19},{call,qc_leveldb,reopen,[]}}
+        Reply: {ptr,{struct,leveldb_t},16831776}
+        State: {state,qc_statemc_lets,{state,false,true,undefined,[]}}
+
+ #11:
+        Cmd: {set,{var,22},{call,qc_leveldb,delete,[{var,19},<<>>]}}
+        Reply: true
+        State: {state,qc_statemc_lets,
+                      {state,false,true,{ptr,{struct,leveldb_t},16831776},[]}}
+
+ #12:
+        Cmd: {set,{var,26},{call,qc_leveldb,close,[{var,19}]}}
+        Reply: true
+        State: {state,qc_statemc_lets,
+                      {state,false,true,{ptr,{struct,leveldb_t},16831776},[]}}
+
+ #13:
+        Cmd: {set,{var,27},{call,qc_leveldb,reopen,[]}}
+        Reply: {ptr,{struct,leveldb_t},16831712}
+        State: {state,qc_statemc_lets,{state,false,true,undefined,[]}}
+
+ #14:
+        Cmd: {set,{var,31},{call,qc_leveldb,put,[{var,27},{obj,<<>>,<<>>}]}}
+        Reply: true
+        State: {state,qc_statemc_lets,
+                      {state,false,true,{ptr,{struct,leveldb_t},16831712},[]}}
+
+ #15:
+        Cmd: {set,{var,33},{call,qc_leveldb,close,[{var,27}]}}
+        Reply: true
+        State: {state,qc_statemc_lets,
+                      {state,false,true,
+                             {ptr,{struct,leveldb_t},16831712},
+                             [{obj,<<>>,<<>>}]}}
+
+ #16:
+        Cmd: {set,{var,34},{call,qc_leveldb,reopen,[]}}
+        Reply: {ptr,{struct,leveldb_t},16832720}
+        State: {state,qc_statemc_lets,
+                      {state,false,true,undefined,[{obj,<<>>,<<>>}]}}
+
+ #17:
+        Cmd: {set,{var,36},{call,qc_leveldb,close,[{var,34}]}}
+        Reply: true
+        State: {state,qc_statemc_lets,
+                      {state,false,true,
+                             {ptr,{struct,leveldb_t},16832720},
+                             [{obj,<<>>,<<>>}]}}
+
+ #18:
+        Cmd: {set,{var,37},{call,qc_leveldb,reopen,[]}}
+        Reply: {ptr,{struct,leveldb_t},16828000}
+        State: {state,qc_statemc_lets,
+                      {state,false,true,undefined,[{obj,<<>>,<<>>}]}}
+
+ #19:
+        Cmd: {set,{var,40},{call,qc_leveldb,last,[{var,37}]}}
+        Reply: <<"a">>
+        State: {state,qc_statemc_lets,
+                      {state,false,true,
+                             {ptr,{struct,leveldb_t},16828000},
+                             [{obj,<<>>,<<>>}]}}
+
+RESULT:
+        {postcondition,false}
+
+STATE:
+        {state,qc_statemc_lets,
+               {state,false,true,
+                      {ptr,{struct,leveldb_t},16828000},
+                      [{obj,<<>>,<<>>}]}}
+
+STATE IS SANE:
+        true
+false
+*/
diff --git a/priv/test/qc_statemc_lets.c b/priv/test/qc_statemc_lets.c
new file mode 100644
index 0000000..4267c56
--- /dev/null
+++ b/priv/test/qc_statemc_lets.c
@@ -0,0 +1,465 @@
+// %%% The MIT License
+// %%%
+// %%% Copyright (C) 2011 by Joseph Wayne Norton <norton@alum.mit.edu>
+// %%%
+// %%% Permission is hereby granted, free of charge, to any person obtaining a copy
+// %%% of this software and associated documentation files (the "Software"), to deal
+// %%% in the Software without restriction, including without limitation the rights
+// %%% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+// %%% copies of the Software, and to permit persons to whom the Software is
+// %%% furnished to do so, subject to the following conditions:
+// %%%
+// %%% The above copyright notice and this permission notice shall be included in
+// %%% all copies or substantial portions of the Software.
+// %%%
+// %%% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+// %%% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+// %%% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+// %%% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+// %%% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+// %%% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+// %%% THE SOFTWARE.
+
+#include <assert.h>
+#include <stdlib.h>
+#include <string.h>
+
+#include "qc_statemc_lets.h"
+
+
+// %%%===================================================================
+// %%% API
+// %%%===================================================================
+//
+// setup() ->
+//     Options = [{c_src,"../c_src/leveldb/include/leveldb/c.h"},
+//                {additional_files, ["../c_src/leveldb/lib/libleveldb.a", "../c_src/snappy/lib/libsnappy.a"]},
+//                {cflags, "-lstdc++ -lpthread"}],
+//     eqc_c:start(leveldb, Options).
+//
+// teardown() ->
+//     os:cmd("rm -rf " ++ ?MODULE_STRING).
+//
+// is_db({ptr, {struct, leveldb_t}, _}) ->
+//     true;
+// is_db(_) ->
+//     false.
+
+
+// open() ->
+//     Options = leveldb:leveldb_options_create(),
+//     try
+//         Leveldb:leveldb_options_set_create_if_missing(Options, 1),
+//         leveldb:leveldb_options_set_error_if_exists(Options, 1),
+//         open(Options)
+//     after
+//         leveldb:leveldb_options_destroy(Options)
+//     end.
+
+leveldb_t* open0() {
+    leveldb_options_t* Options = leveldb_options_create();
+    leveldb_options_set_create_if_missing(Options, 1);
+    leveldb_options_set_error_if_exists(Options, 1);
+    leveldb_t* Db = open1(Options);
+    leveldb_options_destroy(Options);
+    return Db;
+}
+
+
+// open(Options) ->
+//     ErrPtr = errptr(),
+//     try
+//         case leveldb:leveldb_open(Options, ?MODULE_STRING, ErrPtr) of
+//             {ptr, {struct, leveldb_t}, 0} ->
+//                 read_errptr(ErrPtr);
+//             {ptr, {struct, leveldb_t}, _}=Db ->
+//                 Db
+//         end
+//     after
+//         free_ptr(ErrPtr)
+//     end.
+
+leveldb_t* open1(leveldb_options_t* Options) {
+    char* ErrPtr = NULL;
+    leveldb_t* Db = leveldb_open(Options, "qc_leveldb", &ErrPtr);
+    assert(ErrPtr == NULL);
+    return Db;
+}
+
+
+// reopen() ->
+//     Options = leveldb:leveldb_options_create(),
+//     try
+//         reopen(Options)
+//     after
+//         leveldb:leveldb_options_destroy(Options)
+//     end.
+
+leveldb_t* reopen0() {
+    leveldb_options_t* Options = leveldb_options_create();
+    leveldb_t* Db = reopen1(Options);
+    leveldb_options_destroy(Options);
+    return Db;
+}
+
+
+// reopen(Options) ->
+//     ErrPtr = errptr(),
+//     try
+//         case leveldb:leveldb_open(Options, ?MODULE_STRING, ErrPtr) of
+//             {ptr, {struct, leveldb_t}, 0} ->
+//                 read_errptr(ErrPtr);
+//             {ptr, {struct, leveldb_t}, _}=Db ->
+//                 Db
+//         end
+//     after
+//         free_ptr(ErrPtr)
+//     end.
+
+leveldb_t* reopen1(leveldb_options_t* Options) {
+    char* ErrPtr = NULL;
+    leveldb_t* Db = leveldb_open(Options, "qc_leveldb", &ErrPtr);
+    assert(ErrPtr == NULL);
+    return Db;
+}
+
+
+// close(Db) ->
+//     ok == leveldb:leveldb_close(Db).
+
+void close1(leveldb_t* Db) {
+    leveldb_close(Db);
+    return;
+}
+
+
+// put(Db, Obj) ->
+//     Options = leveldb:leveldb_writeoptions_create(),
+//     try
+//         put(Db, Options, Obj)
+//     after
+//         leveldb:leveldb_writeoptions_destroy(Options)
+//     end.
+
+void put2(leveldb_t* Db, char* Key, size_t KeyLen, char* Val, size_t ValLen) {
+    leveldb_writeoptions_t* Options = leveldb_writeoptions_create();
+    put3(Db, Key, KeyLen, Val, ValLen, Options);
+    leveldb_writeoptions_destroy(Options);
+    return;
+}
+
+
+// put(Db, Options, {obj,Key,Val}) ->
+//     ErrPtr = errptr(),
+//     try
+//         leveldb:leveldb_put(Db, Options, binary_to_list(Key), byte_size(Key), binary_to_list(Val), byte_size(Val), ErrPtr),
+//         read_errptr(ErrPtr)
+//     after
+//         free_ptr(ErrPtr)
+//     end.
+
+void put3(leveldb_t* Db, char* Key, size_t KeyLen, char* Val, size_t ValLen, const leveldb_writeoptions_t* Options) {
+    char* ErrPtr = NULL;
+    leveldb_put(Db, Options, Key, KeyLen, Val, ValLen, &ErrPtr);
+    assert(ErrPtr == NULL);
+    return;
+}
+
+
+// delete(Db, Key) ->
+//     Options = leveldb:leveldb_writeoptions_create(),
+//     try
+//         delete(Db, Options, Key)
+//     after
+//         leveldb:leveldb_writeoptions_destroy(Options)
+//     end.
+
+void delete2(leveldb_t* Db, char* Key, size_t KeyLen) {
+    leveldb_writeoptions_t* Options = leveldb_writeoptions_create();
+    delete3(Db, Key, KeyLen, Options);
+    leveldb_writeoptions_destroy(Options);
+    return;
+}
+
+
+// delete(Db, Options, Key) ->
+//     ErrPtr = errptr(),
+//     try
+//         leveldb:leveldb_delete(Db, Options, binary_to_list(Key), byte_size(Key), ErrPtr),
+//         read_errptr(ErrPtr)
+//     after
+//         free_ptr(ErrPtr)
+//     end.
+
+void delete3(leveldb_t* Db, char* Key, size_t KeyLen, const leveldb_writeoptions_t* Options) {
+    char* ErrPtr = NULL;
+    leveldb_delete(Db, Options, Key, KeyLen, &ErrPtr);
+    assert(ErrPtr == NULL);
+    return;
+}
+
+
+// get(Db, Key) ->
+//     Options = leveldb:leveldb_readoptions_create(),
+//     try
+//         get(Db, Options, Key)
+//     after
+//         leveldb:leveldb_readoptions_destroy(Options)
+//     end.
+
+
+char* get2(leveldb_t* Db, char* Key, size_t KeyLen, size_t* ValLen) {
+    leveldb_readoptions_t* Options = leveldb_readoptions_create();
+    char* Val = get3(Db, Key, KeyLen, ValLen, Options);
+    leveldb_readoptions_destroy(Options);
+    return Val;
+}
+
+
+// get(Db, Options, Key) ->
+//     ErrPtr = errptr(),
+//     LenPtr = lenptr(),
+//     try
+//         case leveldb:leveldb_get(Db, Options, binary_to_list(Key), byte_size(Key), LenPtr, ErrPtr) of
+//             0 ->
+//                 read_errptr(ErrPtr);
+//             ValPtr ->
+//                 read_binary(ValPtr, LenPtr)
+//         end
+//     after
+//         free_ptr(ErrPtr),
+//         free_ptr(LenPtr)
+//     end.
+
+
+char* get3(leveldb_t* Db, char* Key, size_t KeyLen, size_t* ValLen, const leveldb_readoptions_t* Options) {
+    char* ErrPtr = NULL;
+    char* Val = leveldb_get(Db, Options, Key, KeyLen, ValLen, &ErrPtr);
+    assert(ErrPtr == NULL);
+    return Val;
+}
+
+
+// first(Db) ->
+//     Options = leveldb:leveldb_readoptions_create(),
+//     try
+//         first(Db, Options)
+//     after
+//         leveldb:leveldb_readoptions_destroy(Options)
+//     end.
+
+char* first1(leveldb_t* Db, size_t *KeyLen) {
+    leveldb_readoptions_t* Options = leveldb_readoptions_create();
+    char* Key = first2(Db, KeyLen, Options);
+    leveldb_readoptions_destroy(Options);
+    return Key;
+}
+
+
+// first(Db, Options) ->
+//     Iter = leveldb:leveldb_create_iterator(Db, Options),
+//     LenPtr = lenptr(),
+//     try
+//         leveldb:leveldb_iter_seek_to_first(Iter),
+//         case leveldb:leveldb_iter_valid(Iter) of
+//             0 ->
+//                 true;
+//             1 ->
+//                 KeyPtr = leveldb:leveldb_iter_key(Iter, LenPtr),
+//                 read_binary(KeyPtr, LenPtr)
+//         end
+//     after
+//         leveldb:leveldb_iter_destroy(Iter),
+//         free_ptr(LenPtr)
+//     end.
+
+char* first2(leveldb_t* Db, size_t* KeyLen, const leveldb_readoptions_t* Options) {
+    leveldb_iterator_t* Iter = leveldb_create_iterator(Db, Options);
+    char* Key = NULL;
+    *KeyLen = 0;
+
+    leveldb_iter_seek_to_first(Iter);
+    if (leveldb_iter_valid(Iter)) {
+        Key = (char*) leveldb_iter_key(Iter, KeyLen);
+        Key = read_binary(Key, KeyLen);
+    }
+
+    leveldb_iter_destroy(Iter);
+    return Key;
+}
+
+// last(Db) ->
+//     Options = leveldb:leveldb_readoptions_create(),
+//     try
+//         last(Db, Options)
+//     after
+//         leveldb:leveldb_readoptions_destroy(Options)
+//     end.
+
+char* last1(leveldb_t* Db, size_t *KeyLen) {
+    leveldb_readoptions_t* Options = leveldb_readoptions_create();
+    char* Key = last2(Db, KeyLen, Options);
+    leveldb_readoptions_destroy(Options);
+    return Key;
+}
+
+
+// last(Db, Options) ->
+//     Iter = leveldb:leveldb_create_iterator(Db, Options),
+//     LenPtr = lenptr(),
+//     try
+//         leveldb:leveldb_iter_seek_to_last(Iter),
+//         case leveldb:leveldb_iter_valid(Iter) of
+//             0 ->
+//                 true;
+//             1 ->
+//                 KeyPtr = leveldb:leveldb_iter_key(Iter, LenPtr),
+//                 read_binary(KeyPtr, LenPtr)
+//         end
+//     after
+//         leveldb:leveldb_iter_destroy(Iter),
+//         free_ptr(LenPtr)
+//     end.
+
+char* last2(leveldb_t* Db, size_t* KeyLen, const leveldb_readoptions_t* Options) {
+    leveldb_iterator_t* Iter = leveldb_create_iterator(Db, Options);
+    char* Key = NULL;
+    *KeyLen = 0;
+
+    leveldb_iter_seek_to_last(Iter);
+    if (leveldb_iter_valid(Iter)) {
+        Key = (char*) leveldb_iter_key(Iter, KeyLen);
+        Key = read_binary(Key, KeyLen);
+    }
+
+    leveldb_iter_destroy(Iter);
+    return Key;
+}
+
+
+// next(Db, Key) ->
+//     Options = leveldb:leveldb_readoptions_create(),
+//     try
+//         next(Db, Key, Options)
+//     after
+//         leveldb:leveldb_readoptions_destroy(Options)
+//     end.
+
+char* next2(leveldb_t* Db, char* Key, size_t KeyLen, size_t *NextKeyLen) {
+    leveldb_readoptions_t* Options = leveldb_readoptions_create();
+    char* NextKey = next3(Db, Key, KeyLen, NextKeyLen, Options);
+    leveldb_readoptions_destroy(Options);
+    return NextKey;
+}
+
+
+// next(Db, Key, Options) ->
+//     Iter = leveldb:leveldb_create_iterator(Db, Options),
+//     LenPtr = lenptr(),
+//     LenPtr1 = lenptr(),
+//     try
+//         leveldb:leveldb_iter_seek(Iter, binary_to_list(Key), byte_size(Key)),
+//         case leveldb:leveldb_iter_valid(Iter) of
+//             0 ->
+//                 true;
+//             1 ->
+//                 KeyPtr = leveldb:leveldb_iter_key(Iter, LenPtr),
+//                 K = read_binary(KeyPtr, LenPtr),
+//                 if K =/= Key ->
+//                         K;
+//                    true ->
+//                         leveldb:leveldb_iter_next(Iter),
+//                         case leveldb:leveldb_iter_valid(Iter) of
+//                             0 ->
+//                                 true;
+//                             1 ->
+//                                 KeyPtr1 = leveldb:leveldb_iter_key(Iter, LenPtr1),
+//                                 read_binary(KeyPtr1, LenPtr1)
+//                         end
+//                 end
+//         end
+//     after
+//         leveldb:leveldb_iter_destroy(Iter),
+//         free_ptr(LenPtr),
+//         free_ptr(LenPtr1)
+//     end.
+
+char* next3(leveldb_t* Db, char* Key, size_t KeyLen, size_t* NextKeyLen, const leveldb_readoptions_t* Options) {
+    leveldb_iterator_t* Iter = leveldb_create_iterator(Db, Options);
+    char* NextKey = NULL;
+    *NextKeyLen = 0;
+
+    leveldb_iter_seek(Iter, Key, KeyLen);
+    if (leveldb_iter_valid(Iter)) {
+        NextKey = (char*) leveldb_iter_key(Iter, NextKeyLen);
+
+        if (0 == compare_binary(Key, KeyLen, NextKey, *NextKeyLen)) {
+            leveldb_iter_next(Iter);
+
+            if (leveldb_iter_valid(Iter)) {
+                NextKey = (char*) leveldb_iter_key(Iter, NextKeyLen);
+                NextKey = read_binary(NextKey, NextKeyLen);
+            } else {
+                NextKey = NULL;
+                *NextKeyLen = 0;
+            }
+        } else {
+            NextKey = read_binary(NextKey, NextKeyLen);
+        }
+    }
+
+    leveldb_iter_destroy(Iter);
+    return NextKey;
+}
+
+// %%%===================================================================
+// %%% Internal
+// %%%===================================================================
+//
+// errptr() ->
+//     eqc_c:alloc({ptr, char}, [0]).
+//
+// lenptr() ->
+//     eqc_c:alloc(unsigned_long, 0).
+//
+// free_ptr(Ptr) ->
+//     eqc_c:free(Ptr).
+//
+// read_errptr(ErrPtr) ->
+//     case eqc_c:read_string(eqc_c:deref(ErrPtr)) of
+//         [] ->
+//             true;
+//         Err ->
+//             Err
+//     end.
+//
+// read_lenptr(LenPtr) ->
+//     eqc_c:deref(LenPtr).
+//
+// read_binary({ptr, char, 0}, _LenPtr) ->
+//     true;
+// read_binary(ValPtr, LenPtr) ->
+//     list_to_binary(eqc_c:read_array(ValPtr, read_lenptr(LenPtr))).
+
+
+char* read_binary(const char* B, size_t* BLen) {
+    char* tmp = malloc(*BLen);
+    if (tmp) {
+        tmp = memcpy(tmp, B, *BLen);
+    } else {
+        *BLen = 0;
+    }
+
+    return tmp;
+}
+
+
+int compare_binary(const char* A, size_t ALen, const char* B, size_t BLen) {
+    if (ALen > BLen) {
+        return 1;
+    } else if (ALen < BLen) {
+        return -1;
+    } else {
+        return memcmp(A, B, ALen);
+    }
+}
diff --git a/priv/test/qc_statemc_lets.h b/priv/test/qc_statemc_lets.h
new file mode 100644
index 0000000..6b5de63
--- /dev/null
+++ b/priv/test/qc_statemc_lets.h
@@ -0,0 +1,76 @@
+// %%% The MIT License
+// %%%
+// %%% Copyright (C) 2011 by Joseph Wayne Norton <norton@alum.mit.edu>
+// %%%
+// %%% Permission is hereby granted, free of charge, to any person obtaining a copy
+// %%% of this software and associated documentation files (the "Software"), to deal
+// %%% in the Software without restriction, including without limitation the rights
+// %%% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+// %%% copies of the Software, and to permit persons to whom the Software is
+// %%% furnished to do so, subject to the following conditions:
+// %%%
+// %%% The above copyright notice and this permission notice shall be included in
+// %%% all copies or substantial portions of the Software.
+// %%%
+// %%% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+// %%% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+// %%% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+// %%% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+// %%% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+// %%% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+// %%% THE SOFTWARE.
+
+#ifndef QC_STATEMC_LETS_H
+#define QC_STATEMC_LETS_H
+
+#include "leveldb/c.h"
+
+// -module(qc_leveldb).
+//
+// %% API
+// -export([%% test
+//          setup/0
+//          , teardown/0
+//          , is_db/1
+//          %% lets
+//          , open/0, open/1
+//          , reopen/0, reopen/1
+//          , close/1
+//          , put/2, put/3
+//          , delete/2, delete/3
+//          , get/2, get/3
+//          , first/1, first/2
+//          , last/1, last/2
+//          , next/2, next/3
+//         ]).
+
+extern leveldb_t* open0();
+extern leveldb_t* open1(leveldb_options_t* Options);
+
+extern leveldb_t* reopen0();
+extern leveldb_t* reopen1(leveldb_options_t* Options);
+
+extern void close1(leveldb_t* Db);
+
+extern void put2(leveldb_t* Db, char* Key, size_t KeyLen, char* Val, size_t ValLen);
+extern void put3(leveldb_t* Db, char* Key, size_t KeyLen, char* Val, size_t ValLen, const leveldb_writeoptions_t* Options);
+
+extern void delete2(leveldb_t* Db, char* Key, size_t KeyLen);
+extern void delete3(leveldb_t* Db, char* Key, size_t KeyLen, const leveldb_writeoptions_t* Options);
+
+extern char* get2(leveldb_t* Db, char* Key, size_t KeyLen, size_t* ValLen);
+extern char* get3(leveldb_t* Db, char* Key, size_t KeyLen, size_t* ValLen, const leveldb_readoptions_t* Options);
+
+extern char* first1(leveldb_t* Db, size_t *KeyLen);
+extern char* first2(leveldb_t* Db, size_t* KeyLen, const leveldb_readoptions_t* Options);
+
+extern char* last1(leveldb_t* Db, size_t *KeyLen);
+extern char* last2(leveldb_t* Db, size_t* KeyLen, const leveldb_readoptions_t* Options);
+
+extern char* next2(leveldb_t* Db, char* Key, size_t KeyLen, size_t* NextKeyLen);
+extern char* next3(leveldb_t* Db, char* Key, size_t KeyLen, size_t* NextKeyLen, const leveldb_readoptions_t* Options);
+
+extern char* read_binary(const char* B, size_t* BLen);
+extern int compare_binary(const char* A, size_t ALen, const char* B, size_t BLen);
+
+#endif /* QC_STATEMC_LETS_H */
diff --git a/priv/test/qc_statemc_leveldb_issue44.erl b/priv/test/qc_statemc_leveldb_issue44.erl
new file mode 100644
index 0000000..faeefbe
--- /dev/null
+++ b/priv/test/qc_statemc_leveldb_issue44.erl
@@ -0,0 +1,21 @@
+[{init,{state,qc_statemc_lets,{state,false,false,undefined,[]}}},
+ {set,{var,1},{call,qc_leveldb,open,[]}},
+ {set,{var,4},{call,qc_leveldb,close,[{var,1}]}},
+ {set,{var,5},{call,qc_leveldb,reopen,[]}},
+ {set,{var,6},{call,qc_leveldb,put,[{var,5},{obj,<<"a">>,<<>>}]}},
+ {set,{var,9},{call,qc_leveldb,close,[{var,5}]}},
+ {set,{var,10},{call,qc_leveldb,reopen,[]}},
+ {set,{var,11},{call,qc_leveldb,delete,[{var,10},<<"a">>]}},
+ {set,{var,14},{call,qc_leveldb,delete,[{var,10},<<>>]}},
+ {set,{var,15},{call,qc_leveldb,close,[{var,10}]}},
+ {set,{var,19},{call,qc_leveldb,reopen,[]}},
+ {set,{var,22},{call,qc_leveldb,delete,[{var,19},<<>>]}},
+ {set,{var,26},{call,qc_leveldb,close,[{var,19}]}},
+ {set,{var,27},{call,qc_leveldb,reopen,[]}},
+ {set,{var,31},{call,qc_leveldb,put,[{var,27},{obj,<<>>,<<>>}]}},
+ {set,{var,33},{call,qc_leveldb,close,[{var,27}]}},
+ {set,{var,34},{call,qc_leveldb,reopen,[]}},
+ {set,{var,36},{call,qc_leveldb,close,[{var,34}]}},
+ {set,{var,37},{call,qc_leveldb,reopen,[]}},
+ {set,{var,40},{call,qc_leveldb,last,[{var,37}]}}
+].
diff --git a/test/qc/qc_leveldb.erl b/test/qc/qc_leveldb.erl
index 7d74a72..3ae4475 100644
--- a/test/qc/qc_leveldb.erl
+++ b/test/qc/qc_leveldb.erl
@@ -48,7 +48,11 @@ setup() ->
     Options = [{c_src,"../c_src/leveldb/include/leveldb/c.h"},
                {additional_files, ["../c_src/leveldb/lib/libleveldb.a", "../c_src/snappy/lib/libsnappy.a"]},
                {cflags, "-lstdc++ -lpthread"}],
-    eqc_c:start(leveldb, Options).
+    DebugOptions = [%% verbose
+                    %% valgrind , {exec_command_line, fun(Exe) -> {os:find_executable("valgrind"), [Exe]} end}
+                   ],
+    eqc_c:start(leveldb, Options ++ DebugOptions).
+    %% eqc_c:start(leveldb, Options).
 
 teardown() ->
     os:cmd("rm -rf " ++ ?MODULE_STRING).
diff --git a/test/qc/qc_statem_lets.erl b/test/qc/qc_statem_lets.erl
index 378a31b..76c4424 100644
--- a/test/qc/qc_statem_lets.erl
+++ b/test/qc/qc_statem_lets.erl
@@ -82,6 +82,7 @@ serial_command_gen(_Mod,#state{tab=Tab, type=Type}=S) ->
     oneof([{call,?IMPL,insert,[Tab,oneof([gen_obj(S),gen_objs(S)])]}]
           ++ [{call,?IMPL,insert_new,[Tab,oneof([gen_obj(S),gen_objs(S)])]} || Type == ets]
           %% @TODO ++ [{call,?IMPL,delete,[Tab]}]
+          ++ [{call,?IMPL,delete,[Tab]}]
           ++ [{call,?IMPL,delete,[Tab,gen_key(S)]}]
           ++ [{call,?IMPL,delete_all_objs,[Tab]} || Type == ets]
           ++ [{call,?IMPL,lookup,[Tab,gen_key(S)]}]