Various architectural changes

[helm.git] / helm / software / components / ng_paramodulation / superposition.ml

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 67df0654ecf88bf3d0f73d5f7279700b9ec45a7d..306104658414913ece8eef01a984f462c86bb240 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -194,6 +194,7 @@ module Superposition (B : Orderings.Blob) =
 
     let demodulate_once ~jump_to_right bag (id, nlit, plit, vl, pr) table =
      match nlit,plit with
+     |[literal,_], []
      |[],[literal,_] ->
       (match literal with
       | Terms.Predicate t -> assert false
@@ -259,8 +260,7 @@ module Superposition (B : Orderings.Blob) =
       | _, [], [Terms.Equation (l,r,_,_),_], vl, proof when unify ->
           (try ignore(Unif.unification (* vl *) [] l r); true
           with FoUnif.UnificationFailure _ -> false)
-      | _, [], [Terms.Equation (_,_,_,_),_], _, _ -> false
-      | _ -> assert false
+      | _ -> false
     ;;
 
     let build_new_clause bag maxvar filter rule t subst id id2 pos dir =