diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-06 15:32:32 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-06 15:45:38 -0400 |
| commit | 5b2fc4b690f9358dac09b057285c54a6df7c543e (patch) | |
| tree | 727bec817ecb579a0fb8fd2a6a833af857c3f3df /src | |
| parent | d344d4874bda7e90692149d6989c8ca63f0db602 (diff) | |
sets: fix equality propagation
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 8c9441483..9b628ede2 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -990,6 +990,7 @@ bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, T if(value) { d_theory.d_termInfoManager->mergeTerms(t1, t2); } + d_theory.propagate( value ? EQUAL(t1, t2) : NOT(EQUAL(t1, t2)) ); return true; } |