projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ef38a3b) | patch
Make sure phase-shift lemma is properly typed (#8824)
authorGereon Kremer <gkremer@cs.stanford.edu>
Thu, 26 May 2022 16:45:13 +0000 (09:45 -0700)
committerGitHub <noreply@github.com>
Thu, 26 May 2022 16:45:13 +0000 (16:45 +0000)
commita4b9a04373f463607a09c71c26f7dbcad37d219c
tree8706a4d022e12575c25cdce849acc08af090f9bdtree
parentef38a3b721c725eaff2c1dbf9cf828213a853758commit | diff
Make sure phase-shift lemma is properly typed (#8824)

This PR addresses #8773 by making sure that the phase shift lemmas generated by the sine solver are properly typed.
src/theory/arith/nl/transcendental/sine_solver.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/nl/nta/issue8773-phase-shift.smt2 [new file with mode: 0644] blob