anchor.diff:    (cl-cryptominisat::add-clause solver '((0 T)))
     (cl-cryptominisat::add-clause solver '((0) (1)))
     (cl-cryptominisat::solve solver)
  -  (is (cl-cryptominisat::get-model solver) '(NIL T) "should return the assignment of truth values satisfying the SAT problem"))
  +  (is (cl-cryptominisat::get-model solver) '(NIL T) "should return the assignment of truth values satisfying the SAT problem")
  +  (cl-cryptominisat::destroy-solver solver))
   
   (diag "=== get-conflict ===")
   (let ((solver (cl-cryptominisat::create-solver)))
  
positive.code:   (is (cl-cryptominisat::solve solver) T "should return T when a solution is found")
    (cl-cryptominisat::add-clause solver '((0 T) (1 T)))
    (cl-cryptominisat::add-clause solver '((0) (1 T)))
    (is (cl-cryptominisat::solve solver) NIL "should return NIL when a solution cannot be found"))
  
  (diag "=== solve-with-assumptions ===")
  (let ((solver (cl-cryptominisat::create-solver)))
  
negative.code:   (cl-cryptominisat::add-clause solver '((0) (1)))
    (cl-cryptominisat::add-clause solver '((0 T) (1)))
    (is (cl-cryptominisat::solve-with-assumptions solver '((1 T))) NIL "should return NIL when a solution cannot be found")
    (is (cl-cryptominisat::solve-with-assumptions solver '((0 T))) T "should return T when a solution is found")
    (cl-cryptominisat::destroy-solver solver))
  
  (diag "=== get-model ===")
  (let ((solver (cl-cryptominisat::create-solver)))
  