summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2017-11-13 06:15:03 -0800
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2017-11-13 08:15:03 -0600
commit0f0e54c8581209d7c0e85072654b6dbd3c57c5d3 (patch)
treed5a7ee750f1bbcef1da57d06427e4f96bccb45e4
parentf42bc238ff09173af2c917edda7372d99b799a58 (diff)
Initializing SortInference::initialSortCount. Resolves 1172053. (#1357)
-rw-r--r--src/theory/sort_inference.h5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h
index ae4131fa8..c4d898dac 100644
--- a/src/theory/sort_inference.h
+++ b/src/theory/sort_inference.h
@@ -90,8 +90,9 @@ private:
Node mkInjection( TypeNode tn1, TypeNode tn2 );
//reset
void reset();
-public:
- SortInference() : sortCount( 1 ){}
+
+ public:
+ SortInference() : sortCount(1), initialSortCount() {}
~SortInference(){}
void simplify( std::vector< Node >& assertions, bool doSortInference, bool doMonotonicyInference );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback