projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b286d64) | patch
Bug fix in justification heuristic. Had to do with how
authorKshitij Bansal <kshitij@cs.nyu.edu>
Fri, 15 Jun 2012 22:15:43 +0000 (22:15 +0000)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Fri, 15 Jun 2012 22:15:43 +0000 (22:15 +0000)
commit86aa93a619e4697b92c719f478399965ccb96d2d
tree50fa20db51b433832480461f6f2b902109538308tree
parentb286d6463eb671d35b81958b18309b8f096c2586commit | diff
Bug fix in justification heuristic. Had to do with how
a "visited" node in the recursive findSplitter method was
handled (which would lead to infinite loop). Earlier,
they were ignored assuming the ancestor would split on it
later. The right thing to do is to split on it right away.

(Fixes errors from the fuzzer, not the ones from last night's
regression)
src/decision/justification_heuristic.cpp diff | blob | history