- Email: Antti.Hyvarinen@gmail.com
- Registered on: 23/10/2012
- Last connection: 30/04/2019
- 15:12 OpenSMT 2 Revision fcef4b25: Fixed the UF interpolation to work with mkUninterpFun instead of the protected function mkFun
- 12:08 OpenSMT 2 Revision a72eb964: Fixed problems with boolean atoms not getting into the egraph solver where needed.
- 12:05 OpenSMT 2 Revision 4c50dd1f: Fixed a problem with distinctions being applied to the node instead of the root of the node. Some tiny cleaning
- 18:34 OpenSMT 2 Revision 771bc674: Fixed a problem with distinct, which assumed that a distinct predicate in merge conflict only contains two equal atoms
- 17:39 OpenSMT 2 Revision cce79478: Fixed what is possibly a performance bug in lookahead, where backjumping inside lookahead computation resulted in restart instead of re-trying the same node.
- 14:48 OpenSMT 2 Revision 11cdca65: Cleaned a little the regression tests
- 14:26 OpenSMT 2 Revision 1a0f7a49: Implemented again the lookahead partitioning. Mostly untested, but might still work.
- 12:29 OpenSMT 2 Revision 85a8c72b: Cleaned code more
- 19:38 OpenSMT 2 Revision b2d96009: Cleaned more the code, separated the splitting code from general lookahead code. The splitting should not yet work correctly.
Also available in: Atom