Fix rewriting of mixed-integer atoms (#8214)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Thu, 3 Mar 2022 00:37:05 +0000 (01:37 +0100)
committerGitHub <noreply@github.com>
Thu, 3 Mar 2022 00:37:05 +0000 (00:37 +0000)
commit91eb86f4f64e29865661bc2edc4fb86317808d16
tree27244064d8bb31d66a31133ef62199815ec7ce85
parenta30458a2a3e21f40e893fe545c6e9c2c73e32707
Fix rewriting of mixed-integer atoms (#8214)

The sixth input from #8159 revealed a subtle issue in our rewriting of arithmetic atoms. As real and integer atoms are rewritten differently, we check this and then call different functions. However, we check this on the original input, although this property can change during rewriting, e.g., when the only real variable vanishes.
This PR fixes this issue.
src/theory/arith/arith_rewriter.cpp
src/theory/arith/rewriter/addition.cpp
src/theory/arith/rewriter/addition.h
src/theory/arith/rewriter/node_utils.cpp
src/theory/arith/rewriter/node_utils.h
src/theory/arith/rewriter/rewrite_atom.cpp
test/regress/CMakeLists.txt
test/regress/regress0/arith/issue8159-rewrite-intreal.smt2 [new file with mode: 0644]