diff options
Diffstat (limited to 'src/theory/quantifiers/ambqi_builder.cpp')
| -rwxr-xr-x | src/theory/quantifiers/ambqi_builder.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index e3f031d11..7f119ae93 100755 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -863,7 +863,7 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) {
Assert( n.getKind()!=FORALL );
- if( n.getKind()==NOT ){
+ if( n.getKind()==NOT && n[0].getKind()!=FORALL ){
doCheck( m, q, ad, n[0] );
ad.negate();
return true;
|