summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2017-11-06 23:18:29 -0800
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2017-11-07 01:18:29 -0600
commit10278e9ec588286705468d72d04bbf03513b3c88 (patch)
tree981a87b8a2f752ecac56c1b0dce7dc05f0e6fc03 /src/theory
parent08d152c052c49ce5759ab9e682ff131172c7879f (diff)
Initializing NegContainsSygusInvarianceTest::d_cpbe in constructor. (#1328)
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/quantifiers/ce_guided_pbe.cpp3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ce_guided_pbe.cpp b/src/theory/quantifiers/ce_guided_pbe.cpp
index cadfbbe86..81e2f9708 100644
--- a/src/theory/quantifiers/ce_guided_pbe.cpp
+++ b/src/theory/quantifiers/ce_guided_pbe.cpp
@@ -1024,8 +1024,9 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >&
*/
class NegContainsSygusInvarianceTest : public quantifiers::SygusInvarianceTest {
public:
- NegContainsSygusInvarianceTest(){}
+ NegContainsSygusInvarianceTest() : d_cpbe(nullptr){}
~NegContainsSygusInvarianceTest(){}
+
/** initialize this invariance test
* cpbe is the conjecture utility.
* e is the enumerator which we are reasoning about (associated with a synth
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback