This commit merges in the branch branches/arithmetic/congruence into trunk. Here are a summary of the changes:

- Adds CDMaybe and CDRaised in cdmaybe.h
- Add test for congruence over arithmetic terms and constants
- Renames DifferenceManager to CongruenceManager
- Changes a number of internal details for CongruenceManager

1 files changed, 15 insertions, 0 deletions

diff --git a/test/regress/regress0/uflra/constants0.smt b/test/regress/regress0/uflra/constants0.smt
new file mode 100644
index 000000000..b07a6bc4e
--- /dev/null
+++ b/test/regress/regress0/uflra/constants0.smt
@@ -0,0 +1,15 @@
+(benchmark mathsat
+:logic QF_UFLRA
+:status unsat 
+:category { crafted } 
+:extrafuns ((f Real Real))
+:extrafuns ((x Real))
+:extrafuns ((y Real))
+:formula
+(and (or (= x 3) (= x 5))
+     (or (= y 3) (= y 5))
+     (not (= (f x) (f y)))
+     (implies (= (f 3) (f x)) (= (f 5) (f x)))
+     (implies (= (f 3) (f y)) (= (f 5) (f y)))
+)
+)
\ No newline at end of file