search

usi-verification-and-security / opensmt

The opensmt solver
Other
77 stars 18 forks source link

Interpolation error during QF_UF resolution #417

Open BritikovKI opened 2 years ago

BritikovKI commented 2 years ago

During the run of the tests with interpolation some of the interpolation builds were failed, even though the case itself was resolved. Current state: Running opensmt ./gensys_icl006_itptest_eufexps.smt2 results in an error: libc++abi: terminating with uncaught exception of type OsmtInternalException: Error in coloring information

Expected behavior: opensmt successfully builds an interpolant.

File can be found here

blishko commented 2 years ago

It seems I can't reproduce this problem. On current master, this example works fine for me and OpenSMT computes interpolant true.

blishko commented 2 years ago

Here is the minimized example capturing the core problem:

(set-option :produce-interpolants true)
(set-logic QF_UF)
(set-option :interpolation-bool-algorithm 1)
(declare-sort U 0)
(declare-fun x () U)
(declare-fun y () U)
(declare-fun f (U) U)

(assert (!(and (= (f y) x) (= (f x) x)):named A))

(assert (!(and (not (= (f y) (f x))) (= (f x) x)):named B))

(check-sat)
(get-interpolants A B)

It looks like the UF interpolation algorithm does not expect literals to be colored AB, but this can easily happen with Pudlak's boolean interpolation algorithm, which is chosen by the option (set-option :interpolation-bool-algorithm 1).

We need to find out if this condition in UF interpolator is necessary for its correctness, and if so, how to deal with shared literals (colored AB).