projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0e7ebfa) | patch
Fix issue 5309 (#5327)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Thu, 22 Oct 2020 16:48:25 +0000 (11:48 -0500)
committerGitHub <noreply@github.com>
Thu, 22 Oct 2020 16:48:25 +0000 (11:48 -0500)
commite09c7d12441e55fe942ae573b49b880431cf1af1
tree58b3a261b8c804fa7aa470240360eb760ff86daatree
parent0e7ebfa3ba5d5049c81b2c5ac113af62c35f5c64commit | diff
Fix issue 5309 (#5327)

This PR fixes #5309 by ensuring singleton terms are added to the model builder as representatives.

Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/theory_model_builder.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sets/issue5309.smt2 [new file with mode: 0644] blob