let rec demodulate bag (id, literal, vl, pr) table =
debug (lazy ("demodulate " ^ (string_of_int id)));
match literal with
- | Terms.Predicate t -> assert false
+ | Terms.Predicate t -> (* assert false *)
+ let bag,_,id1 =
+ visit bag [] (fun x -> x) id t (ctx_demod table vl)
+ in
+ let cl,_,_ = Terms.get_from_bag id1 bag in
+ bag,cl
| Terms.Equation (l,r,ty,_) ->
let bag,l,id1 =
visit bag [2]