From 77874cd68a5168f908494d48b16c6873a36790ef Mon Sep 17 00:00:00 2001
From: Dimitri Lozeve <dimitri.lozeve@gmail.com>
Date: Thu, 4 Aug 2016 20:11:47 +0100
Subject: [PATCH] Removed unnecessary call in solveDPLL

---
 Sat.hs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Sat.hs b/Sat.hs
index 7a2e741..267b37a 100644
--- a/Sat.hs
+++ b/Sat.hs
@@ -219,8 +219,7 @@ solveDPLL (f, asst)
       let (f', asst') = (pureLitRule . unitPropagate) (f, asst) in
         case solveDPLL (evalLit lit f', lit:asst') of
           SAT a -> SAT a
-          UNSAT -> let (f'', asst'') = (pureLitRule . unitPropagate) (f, asst) in
-                     solveDPLL (evalLit (notLit lit) f'', notLit lit : asst'')
+          UNSAT -> solveDPLL (evalLit (notLit lit) f', notLit lit : asst')
 
 -- Select a literal from a given formula. This function just takes the
 -- first available literal. The function head makes it unsafe, as it