Fix casting for arith msum (#8940)

[cvc5.git] / test / regress / cli / regress0 / arith / issue8872-msum-types.smt2

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)