From 9348602f05094b032efb33dfd341721b270380a1 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 9 Nov 2021 19:13:22 -0600
Subject: [PATCH] Fix parsing array constants (#7617)

This generalizes a fix for parsing array constants.

Fixes #7596.
---
 src/parser/smt2/smt2.cpp                      | 25 ++++++++++++++++---
 test/regress/CMakeLists.txt                   |  1 +
 .../arrays/issue7596-define-array-uminus.smt2 |  5 ++++
 3 files changed, 28 insertions(+), 3 deletions(-)
 create mode 100644 test/regress/regress0/arrays/issue7596-define-array-uminus.smt2

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index ef784746c..1fc7a637f 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1011,13 +1011,32 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     // resulting rational here. This also is applied for integral real values
     // like 5.0 which are converted to (/ 5 1) to distinguish them from
     // integer constants. We must ensure numerator and denominator are
-    // constant and the denominator is non-zero.
-    if (constVal.getKind() == api::DIVISION)
+    // constant and the denominator is non-zero. A similar issue happens for
+    // negative integers and reals, with unary minus.
+    bool isNeg = false;
+    if (constVal.getKind() == api::UMINUS)
+    {
+      isNeg = true;
+      constVal = constVal[0];
+    }
+    if (constVal.getKind() == api::DIVISION
+        && constVal[0].getKind() == api::CONST_RATIONAL
+        && constVal[1].getKind() == api::CONST_RATIONAL)
     {
       std::stringstream sdiv;
-      sdiv << constVal[0] << "/" << constVal[1];
+      sdiv << (isNeg ? "-" : "") << constVal[0] << "/" << constVal[1];
       constVal = d_solver->mkReal(sdiv.str());
     }
+    else if (constVal.getKind() == api::CONST_RATIONAL && isNeg)
+    {
+      std::stringstream sneg;
+      sneg << "-" << constVal;
+      constVal = d_solver->mkInteger(sneg.str());
+    }
+    else
+    {
+      constVal = args[0];
+    }
 
     if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort()))
     {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b08b2f6f5..9574628a8 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -109,6 +109,7 @@ set(regress_0_tests
   regress0/arrays/issue3813-massign-assert.smt2
   regress0/arrays/issue3814.smt2
   regress0/arrays/issue4927-unsat-cores.smt2
+  regress0/arrays/issue7596-define-array-uminus.smt2
   regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2
   regress0/arrays/x2.smtv1.smt2
   regress0/arrays/x3.smtv1.smt2
diff --git a/test/regress/regress0/arrays/issue7596-define-array-uminus.smt2 b/test/regress/regress0/arrays/issue7596-define-array-uminus.smt2
new file mode 100644
index 000000000..da21db28e
--- /dev/null
+++ b/test/regress/regress0/arrays/issue7596-define-array-uminus.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status sat)
+(define-fun foo () (Array Int Int) ((as const (Array Int Int)) (- 1)))
+(assert (= (select foo 0) (- 1)))
+(check-sat)
-- 
2.30.2