Fix to bug 497: make justification heuristic's ITE cache context-dependent.
authorMorgan Deters <mdeters@cs.nyu.edu>
Tue, 12 Mar 2013 23:41:28 +0000 (19:41 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Thu, 21 Mar 2013 00:00:55 +0000 (20:00 -0400)
commitb480438b3d39000cfac88eac12922a23f9fccbea
treeab310d8512298a733f8e2d8f4805d06ee126208e
parent6106f021745ffc7ebc068f762a196140deb9d48d
Fix to bug 497: make justification heuristic's ITE cache context-dependent.
src/decision/decision_engine.cpp
src/decision/decision_engine.h
src/decision/justification_heuristic.cpp
src/decision/justification_heuristic.h
test/regress/regress0/Makefile.am
test/regress/regress0/bug497.cvc [new file with mode: 0644]