projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 67dc3b9) | patch
attempt to fix bug 293: if a split on a trivial shared pair is requested from a theor...
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Sat, 10 Dec 2011 06:05:13 +0000 (06:05 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Sat, 10 Dec 2011 06:05:13 +0000 (06:05 +0000)
commit48b147577ba6a894f8f0498c39c7e77d466b0538
treee13ec9eb56af775363228fbdd03164ae652273abtree
parent67dc3b98a30a6ad2f93743f3313ba5f4149af389commit | diff
attempt to fix bug 293: if a split on a trivial shared pair is requested from a theory, such as 1 = 0, it is reasserted to the theory.
src/theory/theory_engine.cpp diff | blob | history
test/regress/regress0/uflra/Makefile [new file with mode: 0644] blob
test/regress/regress0/uflra/Makefile.am diff | blob | history
test/regress/regress0/uflra/bug293.cvc [new file with mode: 0644] blob