projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: def4b45) | patch
Make conjecture generator's uf term enumeration safer (#2172)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 1 Aug 2018 07:31:49 +0000 (02:31 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Wed, 1 Aug 2018 07:31:49 +0000 (00:31 -0700)
commit7291952f49ca93bbc98b419d72c20eb45f63c339
tree1e633e865c0c02c0a4358ba6745be6d2ae1318c0tree
parentdef4b45fa41ddf128ab0b2e8f6bb3b8454974008commit | diff
Make conjecture generator's uf term enumeration safer (#2172)

This ensures that the function getEnumerateUfTerm does not have out of bounds accesses. This is an alternative fix to the one brought up in #2158.
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
src/theory/quantifiers/conjecture_generator.h diff | blob | history