projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cf155cb) | patch
Remove spurious assertion in linear solver (#8231)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Fri, 4 Mar 2022 22:31:10 +0000 (23:31 +0100)
committerGitHub <noreply@github.com>
Fri, 4 Mar 2022 22:31:10 +0000 (22:31 +0000)
commit39b607b9c93bc14048bbbff543e8d16534c606f0
treec6480f40711fbd2bce6a81053c6317d0bd967b4dtree
parentcf155cb1cc523eb0885351d18d8ef0c7b221f38fcommit | diff
Remove spurious assertion in linear solver (#8231)

This PR removes a spurious assertion about how integer equality should look like. It actually requires that the coefficients of the leading terms on both sides of the equation are positive, which can't be true in general anyway. Note that the regression failed before we refactored the arithmetic rewriter.

Fixes cvc5/cvc5-projects#469
src/theory/arith/rewriter/rewrite_atom.cpp diff | blob | history
src/theory/arith/theory_arith_private.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/arith/projissue469-int-equality.smt2 [new file with mode: 0644] blob