projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 79cf934) | patch
Make arith msum utility agnostic to Int (#8694)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 2 May 2022 21:58:14 +0000 (16:58 -0500)
committerGitHub <noreply@github.com>
Mon, 2 May 2022 21:58:14 +0000 (21:58 +0000)
commit0e2f84754dd44baa14206780b93f84dd5002a509
tree43b2a3eb62d54bb7535d12a9a36e905c9edf188btree
parent79cf93488f06d8e141463146afc8fcad0cb905f1commit | diff
Make arith msum utility agnostic to Int (#8694)

This utility should continue to assume arithmetic subtypes.

Fixes #8691.
src/theory/arith/arith_msum.cpp diff | blob | history
src/theory/arith/arith_msum.h diff | blob | history
src/theory/arith/arith_rewriter.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/nl/issue8691-3-msum-subtypes.smt2 [new file with mode: 0644] blob
test/regress/cli/regress0/nl/issue8691-msum-subtypes.smt2 [new file with mode: 0644] blob