Commit 5f25e0ed authored by Andrei Paskevich's avatar Andrei Paskevich

split conjunctive premises for alt-ergo

thus we gain more goals than we lose
parent 75779176
......@@ -23,6 +23,7 @@ transformation "eliminate_algebraic_smt"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "split_premise"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment