aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-05-17 13:39:59 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-05-22 15:26:59 +0200
commit7509f5c8eab84fda5a9029329c6b70758259765f (patch)
tree64b2d9b007f2a09ea3e2d1dcec8a774d54437427 /plugins/omega
parenteae11e85b5fe578fbec404b91628062aa255be92 (diff)
ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANT
Diffstat (limited to 'plugins/omega')
-rw-r--r--plugins/omega/omega.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 334b03de1..f655c176f 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -587,10 +587,6 @@ let rec depend relie_on accu = function
end
| [] -> relie_on, accu
-let solve (new_eq_id,new_eq_var,print_var) system =
- try let _ = simplify new_eq_id false system in failwith "no contradiction"
- with UNSOLVABLE -> display_action print_var (snd (depend [] [] (history ())))
-
let negation (eqs,ineqs) =
let diseq,_ = List.partition (fun e -> e.kind = DISE) ineqs in
let normal = function