Fix SRI-CSL#256

Minor update to distributing cheap OR during skolemization.
aman-goel · Jun 26, 2020 · a92a668 · a92a668
1 parent 128e49e
commit a92a668
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 5 deletions.
diff --git a/src/exists_forall/ef_skolemize.c b/src/exists_forall/ef_skolemize.c
@@ -653,11 +653,6 @@ static sk_pair_t *ef_skolemize_term(ef_skolemize_t *sk, term_t t) {
           ivector_push(&args, u);
         }
         result = ef_update_composite(sk, unsigned_term(t), &args);
-
-        d = or_term_desc(terms, result);
-        if (ef_distribute_is_cheap(sk->analyzer, d)) {
-          result = ef_flatten_distribute(sk->analyzer, d, &sk->aux);
-        }
         break;
 
       case FORALL_TERM:
@@ -704,6 +699,12 @@ static sk_pair_t *ef_skolemize_term(ef_skolemize_t *sk, term_t t) {
 
   assert(result != NULL_TERM);
 
+  if (is_pos_term(result) && term_kind(terms, result) == OR_TERM) {
+    d = or_term_desc(terms, result);
+    if (ef_distribute_is_cheap(sk->analyzer, d)) {
+      result = ef_flatten_distribute(sk->analyzer, d, &sk->aux);
+    }
+  }
 
 #if TRACE
   printf("Original (%d): %s\nSkolemized: %s\n", resultq,  yices_term_to_string(t, 120, 1, 0), yices_term_to_string(result, 120, 1, 0));

diff --git a/tests/regress/efsmt/mbqi/issue256.smt2 b/tests/regress/efsmt/mbqi/issue256.smt2
@@ -0,0 +1,6 @@
+(set-logic UF)
+(declare-fun _substvar_41_ () Bool)
+(declare-const v6 Bool)
+(declare-const v7 Bool)
+(assert (=> (and (=> v6 false) (=> v7 v6) v7) _substvar_41_))
+(check-sat)
diff --git a/tests/regress/efsmt/mbqi/issue256.smt2.gold b/tests/regress/efsmt/mbqi/issue256.smt2.gold
@@ -0,0 +1 @@
+sat