From 0e7bcb2e0aa76f17b5f45bf6641bae9d26f8be9e Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 16 Mar 2022 16:21:10 -0700 Subject: [PATCH] Add unit test and assertion to test and catch cvc5-projects/issues/#337. (#7578) --- src/api/cpp/cvc5.cpp | 4 +++- test/unit/api/cpp/solver_black.cpp | 12 ++++++++++-- 2 files changed, 13 insertions(+), 3 deletions(-) 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 -- 2.30.2