summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/theory_quantifiers.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 6a3a6fca1..19a915ae9 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -164,7 +164,7 @@ void TheoryQuantifiers::assertExistential( Node n ){
nb << n[0] << body.notNode();
Node lem = nb;
Trace("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl;
- d_out->lemma( lem );
+ d_out->lemma( lem, false, true );
d_skolemized[n] = true;
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback