From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 16 Mar 2022 23:21:10 +0000 (-0700)
Subject: Add unit test and assertion to test and catch cvc5-projects/issues/#337. (#7578)
X-Git-Tag: cvc5-1.0.0~234
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0e7bcb2e0aa76f17b5f45bf6641bae9d26f8be9e;p=cvc5.git

Add unit test and assertion to test and catch cvc5-projects/issues/#337. (#7578)
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index bef2b9ac9..085eefa8b 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -6606,7 +6606,9 @@ Term Solver::simplify(const Term& term)
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(term);
   //////// all checks before this line
-  return Term(this, d_slv->simplify(*term.d_node));
+  Term res = Term(this, d_slv->simplify(*term.d_node));
+  Assert(res.getSort().d_type->isSubtypeOf(*term.getSort().d_type));
+  return res;
   ////////
   CVC5_API_TRY_CATCH_END;
 }
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 9545c4fb0..3acdecbb8 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -3041,7 +3041,7 @@ TEST_F(TestApiBlackSolver, proj_issue434)
   // the query has free variables, and should throw an exception
   ASSERT_THROW(slv.checkSatAssuming({t1073, t510}), CVC5ApiException);
 }
-  
+
 TEST_F(TestApiBlackSolver, proj_issue436)
 {
   Solver slv;
@@ -3058,7 +3058,7 @@ TEST_F(TestApiBlackSolver, proj_issue436)
   // solve-bv-as-int is incompatible with get-abduct
   ASSERT_THROW(slv.getAbduct(t33), CVC5ApiException);
 }
-  
+
 TEST_F(TestApiBlackSolver, proj_issue431)
 {
   Solver slv;
@@ -3192,5 +3192,13 @@ TEST_F(TestApiBlackSolver, projIssue431)
   abduct = slv.getAbduct(t488);
 }
 
+TEST_F(TestApiBlackSolver, projIssue337)
+{
+  Term t =
+      d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal("3416574625719121610379268"));
+  Term tt = d_solver.simplify(t);
+  ASSERT_EQ(t.getSort(), tt.getSort());
+}
+
 }  // namespace test
 }  // namespace cvc5