[Arith] init demon always merge itself

        case when a new semantical value already
        had a dom was not handled

src/arith.ml

@@ -584,22 +584,7 @@ module DaemonInit = struct
             let norm = CombiSem(Q.one,v,norm) in
             Debug.dprintf4 debug "[Arith] @[normalize %a@ into %a@]@\n"
               Th.print v Th.print v';
-            match Th.normo v' with
-            | Some y ->
-              let pexp =
-                Delayed.mk_pexp d expequality
-                  (ExpCombi(9,sub_cl own0 v',norm)) in
-              Delayed.merge d pexp own0 y;
-              begin match Delayed.get_dom d dom y with
-              | None -> ()
-              | Some vy ->
-                assert (Th.equal vy v');
-                Delayed.set_dom d pexp dom own0 v';
-                let clsem' = ThE.index v' real in
-                attach d clsem' (Bag.elt own0)
-              end
-            | None ->
-              Th.merge_itself d norm own0 v'
+            Th.merge_itself d norm own0 v'
         end;
         Delayed.flush d;
       | _ -> raise UnwaitedEvent

tests/smtlib2/lra/sat/arith_init_always_merge_itself.smt2

+(set-logic QF_LRA)
+(declare-fun v1 () Real)
+(declare-fun v0 () Real)
+(assert
+ (let ((?n2 2))
+ (let ((?n3 4))
+ (let ((?n4 (- v0 v1)))
+ (let ((?n5 (= ?n3 ?n4)))
+ (let ((?n6 (distinct ?n2 v1)))
+ (let ((?n7 (- 2)))
+ (let ((?n8 (* v1 ?n7)))
+ (let ((?n9 (- 4)))
+ (let ((?n10 (= ?n8 ?n9)))
+ (let ((?n11 (= ?n8 ?n3)))
+ (let ((?n12 (- v1)))
+ (let ((?n13 (= ?n2 ?n12)))
+ (let ((?n14 (ite ?n13 ?n4 ?n3)))
+ (let ((?n15 (ite ?n11 ?n9 ?n14)))
+ (let ((?n16 (distinct v1 ?n12)))
+ (let ((?n17 (= ?n2 ?n8)))
+ (let ((?n18 (ite ?n17 ?n4 ?n8)))
+ (let ((?n19 (ite ?n16 ?n2 ?n18)))
+ (let ((?n20 (ite true ?n15 ?n19)))
+ (let ((?n21 (ite ?n10 ?n20 ?n20)))
+ (let ((?n22 (ite ?n6 ?n8 ?n14)))
+ (let ((?n23 (ite ?n6 ?n21 ?n22)))
+ (let ((?n24 (ite ?n5 ?n23 ?n14)))
+ (let ((?n25 (ite ?n6 ?n23 v1)))
+ (let ((?n26 (= ?n24 ?n25)))
+ (let ((?n27 (= ?n3 ?n3)))
+ (let ((?n29 (ite false ?n4 ?n15)))
+ (let ((?n30 (ite ?n27 v1 ?n29)))
+ (let ((?n31 (distinct ?n25 ?n30)))
+ (let ((?n32 (= ?n8 ?n4)))
+ (let ((?n33 (ite ?n32 ?n2 ?n29)))
+ (let ((?n34 (= ?n18 ?n33)))
+ (let ((?n35 (and ?n31 ?n34)))
+ (let ((?n36 (= ?n26 ?n35)))
+ (let ((?n37 (not ?n36))) ?n37
+))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)