diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-10 19:27:05 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-09-10 19:27:05 -0700 |
| commit | 0d997c9351fa1acf0f950c9094fd3e8945d9acf3 (patch) | |
| tree | bbb48d0e1f14596bebb7f045e4af74976cb717bd /src/theory | |
| parent | 1a695dcbe3036ab0f1922c5655c082ec1f14db97 (diff) | |
Set NodeManager to nullptr when exporting vars (#2445)
PR #2409 assumed that temporarily setting the NodeManager to nullptr
when creating variables is not needed anymore. However, this made our
portfolio build fail. This commit reintroduces the temporary NodeManager
change while creating variables.
Diffstat (limited to 'src/theory')
0 files changed, 0 insertions, 0 deletions