From: Tim King <taking@cs.nyu.edu>
Date: Fri, 3 May 2013 17:15:26 +0000 (-0400)
Subject: Merging branch 'soiquickexplain'.
X-Git-Tag: cvc5-1.0.0~7287^2~162
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5100b3d2e8e870f85aaa753b25bd8e1fa2349e39;p=cvc5.git

Merging branch 'soiquickexplain'.
---

5100b3d2e8e870f85aaa753b25bd8e1fa2349e39
diff --cc src/theory/arith/options
index 1366addae,388dcc7ff..35cede8b4
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@@ -91,10 -91,7 +91,14 @@@ option fancyFinal --fancy-final bool :d
  option exportDioDecompositions --dio-decomps bool :default false :read-write
   Let skolem variables for integer divisibility constraints leak from the dio solver.
  
 +option newProp --new-prop bool :default false :read-write
 + Use the new row propagation system
 +
 +option arithPropAsLemmaLength --arith-prop-clauses int :default 8 :read-write
 + Rows shorter than this are propagated as clauses
 +
+ option soiQuickExplain --soi-qe bool :default false :read-write
+  Use quick explain to minimize the sum of infeasibility conflicts.
+ 
++
  endmodule