Bitwuzla may return invalid interpolants

[daniel-raffler]

Hello,

when calculating interpolation sequences, Bitwuzla will sometimes return illegal interpolants. We expect that at every step of the sequence, the interpolant may only use symbols that occur in both partitions. However, some of the interpolants returned by Bitwuzla contain symbols that are not shared.

Here is a simple example:

  private Set<Term> getSymbols(Collection<Term> terms) {
    ImmutableSet.Builder<Term> builder = ImmutableSet.builder();
    var cache = new HashSet<Term>();
    var work = new ArrayDeque<>(terms);
    while (!work.isEmpty()) {
      var term = work.pop();
      if (cache.add(term)) {
        Optional<Kind> kind = Optional.empty();
        try {
          kind = Optional.of(term.kind());
        } catch (IllegalArgumentException e) {
          // Ignore SymFPU symbols
        }

        if (kind.isPresent() && kind.equals(Optional.of(Kind.CONSTANT))) {
          builder.add(term);
        } else if (kind.isPresent() && kind.equals(Optional.of(Kind.APPLY))) {
          for (int c = 1; c < term.num_children(); c++) {
            work.push(term.get(c));
          }
        } else {
          for (int c = 0; c < term.num_children(); c++) {
            work.push(term.get(c));
          }
        }
      }
    }
    return builder.build();
  }

  @Test
  public void itpSymbolTest() {
    Options options = new Options();
    options.set(Option.PRODUCE_INTERPOLANTS, 1);
    options.set(Option.PRODUCE_MODELS, 2);

    var parser = new Parser(termManager, options);

    parser.parse("(declare-const |main::main__x@2| Float64)", true, false);
    parser.parse("(declare-const |main::main__x1@2| Float64)", true, false);
    parser.parse("(declare-const |main::main__x@3| Float64)", true, false);
    parser.parse("(declare-const |main::main__x1@3| Float64)", true, false);

    parser.parse("(declare-const |main::__tmp_1@3| (_ BitVec 32))", true, false);
    parser.parse("(declare-const |main::__VERIFIER_assert__cond@3| (_ BitVec 32))", true, false);

    var t1 =
        parser.parse_term(
            """
                  (and (= |main::main__x@2| (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000))
                       (= |main::main__x1@2|
                          (fp.div RNE |main::main__x@2| (fp #b0 #b10000000000 #b0100000000000000000000000000000000000000000000000000))))
                  """);

    var t2 =
        parser.parse_term(
            """
                  (and (and (not (fp.eq |main::main__x1@2| |main::main__x@2|))
                            (= |main::main__x@3| |main::main__x1@2|))
                        (= |main::main__x1@3|
                            (fp.div RNE |main::main__x@3| (fp #b0 #b10000000000 #b0100000000000000000000000000000000000000000000000000))))
                  """);

    var t3 =
        parser.parse_term(
            """
                  (and (and (and (fp.eq |main::main__x1@3| |main::main__x@3|)
                                  (= |main::__tmp_1@3| (ite (fp.eq |main::main__x@3| (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000)) #b00000000000000000000000000000001 #b00000000000000000000000000000000)))
                            (= |main::__VERIFIER_assert__cond@3| |main::__tmp_1@3|))
                        (= |main::__VERIFIER_assert__cond@3| #b00000000000000000000000000000000))
                  """);

    var solver = parser.bitwuzla();

    solver.assert_formula(t1);
    solver.assert_formula(t2);
    solver.assert_formula(t3);

    assertThat(solver.check_sat()).isEqualTo(Result.UNSAT);

    var itps =
        solver.get_interpolants(
            new Vector_Vector_Term(
                ImmutableList.of(
                    new Vector_Term(ImmutableList.of(t1)),
                    new Vector_Term(ImmutableList.of(t2)),
                    new Vector_Term(ImmutableList.of(t3)))));

    var symF1 = getSymbols(ImmutableList.of(t1));
    var symF2 = getSymbols(ImmutableList.of(t2));
    var symF3 = getSymbols(ImmutableList.of(t3));

    var symI1 = getSymbols(ImmutableList.of(itps.get(0)));
    var symI2 = getSymbols(ImmutableList.of(itps.get(1)));

    assertThat(Sets.intersection(symF1, symF2)).containsAtLeastElementsIn(symI1);
    assertThat(Sets.intersection(symF2, symF3)).containsAtLeastElementsIn(symI2);
  }

Note that this will require Bitwuzla 0.9.1 to work. The output is then:

value of                    : intersection(...)
missing (1)                 : |main::main__x@2|

as the 2nd interpolant contains the symbol |main::main__x@2| which is not in the final formula

[daniel-raffler]

This issue seems to be (partially?) fixed on main. However, there are now 4 segfaults during interpolation