diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-23 15:46:52 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-23 08:46:52 -0500 |
| commit | f8af16037ecb1b9a3c322fc4ea2821497f8a2225 (patch) | |
| tree | bd4078a7c858d3580b3e13e195d1cc8c506b43e4 /src/prop/bvminisat/simp/SimpSolver.h | |
| parent | cea1ad700bc4cff0d9fcfb0f14c8908e24bbc8c2 (diff) | |
Make sure a ReferenceStat is set to values of the correct type (#6430)
This PR fixes a very subtle issue with setting the values a ReferenceStat refers to.
ReferenceStat::set() would take a variable by const& and then store the pointer to it. When giving it a different, but implicitly convertible, type, the pointer would assume the wrong type and consequently read incorrect values from it.
This PR makes set() a template function that explicitly checks that the given type is the correct one.
As we can only export int64_t to the API, this forces users of ReferenceStat to use int64_t stats.
Diffstat (limited to 'src/prop/bvminisat/simp/SimpSolver.h')
| -rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index b103243d3..ec6ed375a 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -114,7 +114,7 @@ class SimpSolver : public Solver { // int merges; int asymm_lits; - int eliminated_vars; + int64_t eliminated_vars; // cvc5::TimerStat total_eliminate_time; protected: |