projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1a97c19) | patch
Make sure conflicts are not rewritten (in arithmetic) (#5219)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Wed, 7 Oct 2020 14:13:41 +0000 (16:13 +0200)
committerGitHub <noreply@github.com>
Wed, 7 Oct 2020 14:13:41 +0000 (09:13 -0500)
commiteb4321c5040258ac1ac41eb955aa5b6b5199011e
tree01524ae48f79b8aa0ab60728e29e3a4b80e92e8ftree
parent1a97c19443833604d57f1453a1bebfe0714d3d8ecommit | diff
Make sure conflicts are not rewritten (in arithmetic) (#5219)

The arithmetic inference manager did rewrite conflicts, which lead to nodes from the conflict not being assumptions (but rewritten assumptions) triggering an assertion. This rewrite is now removed.
Furthermore rewrites triggering the same assertion within the icp subsolver have been refactored to avoid this issue.
src/theory/arith/bound_inference.cpp diff | blob | history
src/theory/arith/inference_id.cpp diff | blob | history
src/theory/arith/inference_manager.cpp diff | blob | history
src/theory/arith/nl/icp/icp_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 [new file with mode: 0644] blob