projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cd5fb80) | patch
Fix model unsoundness for relation join (#7511)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 27 Oct 2021 18:02:52 +0000 (13:02 -0500)
committerGitHub <noreply@github.com>
Wed, 27 Oct 2021 18:02:52 +0000 (18:02 +0000)
commit9c0ec4ead7a013c2da36c16d9d17471d921ca00e
tree6cc97716b62d636aec062af2c40aefa9540dc60etree
parentcd5fb80d86a03ade6037531e52f6c3dd3f708bbfcommit | diff
Fix model unsoundness for relation join  (#7511)

This fixes a model unsoundness issue in the theory solver for relations.
src/theory/inference_id.cpp diff | blob | history
src/theory/inference_id.h diff | blob | history
src/theory/sets/theory_sets_rels.cpp diff | blob | history
src/theory/theory_model_builder.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/rels/qgu-fuzz-relations-1-dd.smt2 [new file with mode: 0644] blob
test/regress/regress0/rels/qgu-fuzz-relations-1.smt2 [new file with mode: 0644] blob