projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e761ec3) | patch
adding an assertion to trigger the problem of bug349 and the testcase
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Sun, 10 Jun 2012 06:09:25 +0000 (06:09 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Sun, 10 Jun 2012 06:09:25 +0000 (06:09 +0000)
commit103d6a6aad30410f8d7546c25c1f5e67f1c334d7
treed3e2a30a59618d38aa8882b1ef09f82170607283tree
parente761ec344a7c9d9b5bff5f312cdb8932083e0bc8commit | diff
adding an assertion to trigger the problem of bug349 and the testcase
bv rewriter apparently deosn't have a proper normal form for equalities
src/theory/theory_engine.cpp diff | blob | history
test/regress/regress0/aufbv/bug349.smt [new file with mode: 0644] blob