projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7d298cf) | patch
fixes for shared term registration. previously the type was not considered when looki...
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Mon, 14 May 2012 20:57:12 +0000 (20:57 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Mon, 14 May 2012 20:57:12 +0000 (20:57 +0000)
commit5b5a421d79d12a31edde3902f2b8ddec6a3ca684
tree738662afe397657be3e793a4f38a9cf0e13f4cd7tree
parent7d298cf9abe3cb09c897eafe6fab5ef636be4c27commit | diff
fixes for shared term registration. previously the type was not considered when looking at theories of the term and for a term like

read(a, f(x))

the term f(x) would not be registered to arithmetic in AUFLIA. this fixies the issue of bug 330 and moves it to some other assertion fail.
src/smt/smt_engine.cpp diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/term_registration_visitor.cpp diff | blob | history
src/theory/theory.h diff | blob | history