From bf53190461b640b64b4864599f3f4a7694995bca Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Jul 2022 15:30:30 -0500
Subject: [PATCH] Fix casting for arith msum (#8940)

Fixes #8872.
---
 src/theory/arith/arith_msum.cpp                     | 13 +++++++++----
 test/regress/cli/CMakeLists.txt                     |  2 ++
 .../cli/regress0/arith/issue8872-2-msum-types.smt2  |  8 ++++++++
 .../cli/regress0/arith/issue8872-msum-types.smt2    | 12 ++++++++++++
 4 files changed, 31 insertions(+), 4 deletions(-)
 create mode 100644 test/regress/cli/regress0/arith/issue8872-2-msum-types.smt2
 create mode 100644 test/regress/cli/regress0/arith/issue8872-msum-types.smt2

diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp
index 354982350..b33b38f19 100644
--- 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 4bfc3bc71..ce49f4aff 100644
--- 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
index 000000000..9abd77472
--- /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
index 000000000..a22cdc2d9
--- /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)
-- 
2.30.2