Fix casting for arith msum (#8940)

Fixes #8872.

diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp
index 354982350b2670df5a2d1487d6a17342ecd61c9d..b33b38f19f7becd907d36edb82648dc5430903cd 100644 (file)
--- a/src/theory/arith/arith_msum.cpp
+++ b/src/theory/arith/arith_msum.cpp
@@ -236,13 +236,18 @@ int ArithMSum::isolate(
     // ensure type is correct for equality
     if (k == EQUAL)
     {
-      if (!vc.getType().isInteger() && val.getType().isInteger())
+      bool vci = vc.getType().isInteger();
+      bool vi = val.getType().isInteger();
+      if (!vci && vi)
       {
         val = nm->mkNode(TO_REAL, val);
       }
-      // note that conversely this utility will never use a real value as
-      // the solution for an integer, thus the types should match now
-      Assert(val.getType() == vc.getType());
+      else if (vci && !vi)
+      {
+        val = nm->mkNode(TO_INTEGER, val);
+      }
+      Assert(val.getType() == vc.getType())
+          << val << " " << vc << " " << val.getType() << " " << vc.getType();
     }
     veq = nm->mkNode(k, inOrder ? vc : val, inOrder ? val : vc);
   }

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 4bfc3bc7100e45724d7739bfb9562b557a167b93..ce49f4aff4708e7c2beeb7d64936284588b6f282 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -69,6 +69,8 @@ set(regress_0_tests
   regress0/arith/issue8159-rewrite-intreal.smt2
   regress0/arith/issue8805-mixed-var-elim.smt2
   regress0/arith/issue8905-pi-to-int.smt2
+  regress0/arith/issue8872-msum-types.smt2
+  regress0/arith/issue8872-2-msum-types.smt2
   regress0/arith/ite-lift.smt2
   regress0/arith/leq.01.smtv1.smt2
   regress0/arith/miplib.cvc.smt2

diff --git a/test/regress/cli/regress0/arith/issue8872-2-msum-types.smt2 b/test/regress/cli/regress0/arith/issue8872-2-msum-types.smt2
new file mode 100644 (file)
index 0000000..9abd774
--- /dev/null
+++ b/test/regress/cli/regress0/arith/issue8872-2-msum-types.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --ext-rew-prep=agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun v () Bool)
+(declare-fun a () Real)
+(declare-fun va () Real)
+(assert (= (- a va) (ite v 0 1)))
+(check-sat)

diff --git a/test/regress/cli/regress0/arith/issue8872-msum-types.smt2 b/test/regress/cli/regress0/arith/issue8872-msum-types.smt2
new file mode 100644 (file)
index 0000000..a22cdc2
--- /dev/null
+++ b/test/regress/cli/regress0/arith/issue8872-msum-types.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --ext-rew-prep=agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () Real)   
+(declare-fun b () Int)     
+(declare-fun c () Int)            
+(declare-fun d () Int)  
+(declare-fun e () Int)  
+(assert (let ((?v_2 (* b 1)))(let ((?v_5 (* c 1)))
+(let ((?v_6 (* (ite (< ?v_2 0) ?v_2 0) (ite (< ?v_5 0) ?v_5 0))))          
+(= (+ (* a d) e) (- ?v_6))))))   
+(check-sat)