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 bef2b9ac95d77c64efeb4b6a37fc588a4f18fcd7..085eefa8b0078d5e0a24dd4183eafd047e74b65d 100644 (file)
--- 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 9545c4fb08960911448a0848ef689c99986ec697..3acdecbb877831eb319d08bc95a2b6c9a9da90f9 100644 (file)
--- 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