[ldv-project] Fwd: MathSAT issues with QF_UFLRA interpolation

Sat Aug 24 15:11:46 MSK 2013

FYI.

To Mikhail and others. The proper list for all LDV project developers is ldv-project at linuxtesting.org when you are going to send something very meaningful outside of ISP RAS (note that I used exactly it in copy for this message). Also it is the most appropriate list to send something from outside ISP RAS to all LDV project developers (so, at the moment it is used in messages with patches to the Linux kernel). Of course the e-mail should be in English and it will be great if before sending it will be verified with some spell checker.

You can subscribe to this list here http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project. Also you can find archives of the list there. 

-------- Beginning of forwarded message  --------
23.08.2013, 21:36, "Mikhail Mandrykin" <mandrykin at ispras.ru>:

Hello!

I work in the Linux Driver Verification project
(http://linuxtesting.org/project/ldv) team, where I've recently implemented a
new kind of c-to-formula encoding for predicate analysis with more precise
handling of pointers, structure fields, small arrays
and finite data structures. The analysis is implemented in the CPAchecker tool
(which uses MathSAT 5 as the default SMT solver) and is  largely
based on the use of uninterpreted functions. So in the latest experiments
I've obtained many interpolation and all-sat problems in QF_UFBV
and QF_UFLRA (QF_UFLIA formulas can also be obtained). In general the
performance of the new approach turned out to be comparable to the usual
encoding with variables+alias analysis. I also encountered
several MathSAT issues with QF_UFLRA and QF_UFBV interpolation and all-sat:
  -- On the QF_UFLRA interpolation problems segfault1.smt2 and segfault2.smt2
(in the attachment) Mathsat 5.2.8 (MathSAT5 version 5.2.8 (4f31ca3f8a5f) (Jul
10 2013 17:52:20, gmp 5.0.5, gcc 4.4.7, 64-bit)) fails with segmentation
fault.
  -- On the  segfault3.smt2 and segfault4.smt2 MathSAT 5 fails with
segmentation fault when run as a library from CPAchecker (the formulas are
dumped from the CPAchecker just before calling MathSAT), but successfully finds
the interpolants when run from the command line, though the options used in
both cases seem to be similar (default with -model_generation=true).
 -- On the QF_UFBV intepolation problem abmixed1_segfault.smt2 MathSAT raises
exception "splitting of AB-mixed terms not supported" when run as a library
from CPAchecker, but fails with segmentation fault when run from the command
line.
  --  There are several examples when a (relatively) medium-sized  QF_UFBV
ALL-SAT problem for 6 predicates takes more than 15 minutes
(allsattimeout.smt2) and examples of very large
interpolants (hugeinterpolant.smt2) obtained for QF_UFBV formulas with
essential arithmetic (bitvector addition) envolved.

I haven't yet compared MathSAT performance with that of other solvers (Z3 and
SmtInterpol) with the new encoding, but already encountered a couple of
examples where mathsat sccessfully solves a formula (in 0.08 s) in which Z3
times out of 3 minutes (justformula.smt2).

Regards,
Mikhail Mandrykin <mandrykin at ispras.ru>,
Linux Driver Verification project,
Institute for System Programming of the Russian Academy of Sciences

--
Linux Verification Center, ISPRAS
web: http://linuxtesting.org

,
(set-info :source |printed by MathSAT|)
(declare-fun PRED13 () Bool)
(declare-fun PRED0 () Bool)
(declare-fun PRED34 () Bool)
(declare-fun |g::__cil_tmp3 at 3| () (_ BitVec 32))
(declare-fun |g::i at 4| () (_ BitVec 32))
(declare-fun PRED17 () Bool)
(declare-fun PRED26 () Bool)
(declare-fun PRED22 () Bool)
(declare-fun PRED23 () Bool)
(declare-fun PRED24 () Bool)
(declare-fun |g::__cil_tmp4 at 3| () (_ BitVec 32))
(declare-fun |main::b at 3| () (_ BitVec 32))
(declare-fun PRED32 () Bool)
(declare-fun PRED25 () Bool)
(declare-fun PRED16 () Bool)
(declare-fun PRED5 () Bool)
(declare-fun *int at 5 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun pstate () (_ BitVec 32))
(declare-fun |*(void)*@5| ((_ BitVec 32)) (_ BitVec 32))
(declare-fun pp () (_ BitVec 32))
(declare-fun *int at 6 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun PRED33 () Bool)
(declare-fun |g::pointer at 2| () (_ BitVec 32))
(declare-fun |g::i at 3| () (_ BitVec 32))
(define-fun .def_7321 () (_ BitVec 32) (bvadd (_ bv1 32) |g::i at 4|))
(define-fun .def_7322 () (_ BitVec 32) (bvshl .def_7321 (_ bv2 32)))
(define-fun .def_7323 () (_ BitVec 32) (bvadd pp .def_7322))
(define-fun .def_7325 () (_ BitVec 32) (|*(void)*@5| .def_7323))
(define-fun .def_10270 () Bool (= |main::b at 3| .def_7325))
(define-fun .def_10274 () Bool (= PRED32 .def_10270))
(define-fun .def_2006 () (_ BitVec 32) (bvshl |g::i at 4| (_ bv2 32)))
(define-fun .def_2069 () (_ BitVec 32) (bvadd pp .def_2006))
(define-fun .def_2070 () (_ BitVec 32) (|*(void)*@5| .def_2069))
(define-fun .def_9984 () Bool (= |main::b at 3| .def_2070))
(define-fun .def_10272 () Bool (= .def_9984 PRED33))
(define-fun .def_1008 () (_ BitVec 32) (|*(void)*@5| pp))
(define-fun .def_9987 () Bool (= |main::b at 3| .def_1008))
(define-fun .def_10173 () Bool (= .def_9987 PRED34))
(define-fun .def_7699 () Bool (= |g::i at 4| (_ bv0 32)))
(define-fun .def_7704 () Bool (= PRED24 .def_7699))
(define-fun .def_7633 () Bool (= |g::i at 4| (_ bv1 32)))
(define-fun .def_7702 () Bool (= .def_7633 PRED25))
(define-fun .def_7698 () Bool (= |g::i at 4| (_ bv2 32)))
(define-fun .def_7700 () Bool (= PRED26 .def_7698))
(define-fun .def_7326 () (_ BitVec 32) (bvmul (_ bv4294967295 32) .def_7325))
(define-fun .def_7327 () (_ BitVec 32) (bvadd |g::pointer at 2| .def_7326))
(define-fun .def_7328 () Bool (= .def_7327 (_ bv4294967295 32)))
(define-fun .def_7331 () Bool (= PRED22 .def_7328))
(define-fun .def_5378 () Bool (= |g::pointer at 2| .def_2070))
(define-fun .def_7329 () Bool (= .def_5378 PRED23))
(define-fun .def_1241 () (_ BitVec 32) (*int at 6 pstate))
(define-fun .def_1846 () Bool (= .def_1241 (_ bv1 32)))
(define-fun .def_5308 () Bool (= .def_1846 PRED13))
(define-fun .def_5305 () Bool (= .def_2006 (_ bv0 32)))
(define-fun .def_5306 () Bool (= PRED16 .def_5305))
(define-fun .def_2007 () (_ BitVec 32) (bvadd pstate .def_2006))
(define-fun .def_2009 () (_ BitVec 32) (*int at 6 .def_2007))
(define-fun .def_2010 () Bool (= .def_2009 (_ bv1 32)))
(define-fun .def_2011 () (_ BitVec 32) (ite .def_2010 (_ bv1 32) (_ bv0 32)))
(define-fun .def_2012 () Bool (= .def_2011 (_ bv0 32)))
(define-fun .def_2014 () Bool (= PRED0 .def_2012))
(define-fun .def_2013 () Bool (= PRED5 .def_2010))
(define-fun .def_2015 () Bool (and .def_2013 .def_2014))
(define-fun .def_5307 () Bool (and .def_2015 .def_5306))
(define-fun .def_5309 () Bool (and .def_5307 .def_5308))
(define-fun .def_2706 () Bool (= |g::pointer at 2| .def_1008))
(define-fun .def_5261 () Bool (= .def_2706 PRED17))
(define-fun .def_5310 () Bool (and .def_5261 .def_5309))
(define-fun .def_7330 () Bool (and .def_5310 .def_7329))
(define-fun .def_7332 () Bool (and .def_7330 .def_7331))
(define-fun .def_7701 () Bool (and .def_7332 .def_7700))
(define-fun .def_7703 () Bool (and .def_7701 .def_7702))
(define-fun .def_7705 () Bool (and .def_7703 .def_7704))
(define-fun .def_10271 () Bool (and .def_7705 .def_10173))
(define-fun .def_10273 () Bool (and .def_10271 .def_10272))
(define-fun .def_10275 () Bool (and .def_10273 .def_10274))
(define-fun .def_381 () (_ BitVec 32) (bvshl |g::i at 3| (_ bv2 32)))
(define-fun .def_382 () (_ BitVec 32) (bvadd pp .def_381))
(define-fun .def_1615 () (_ BitVec 32) (|*(void)*@5| .def_382))
(define-fun .def_10172 () Bool (= |main::b at 3| .def_1615))
(define-fun .def_10227 () Bool (not .def_10172))
(define-fun .def_9988 () Bool (not .def_9987))
(define-fun .def_10228 () Bool (and .def_9988 .def_10227))
(define-fun .def_2000 () (_ BitVec 32) (bvadd (_ bv1 32) |g::i at 3|))
(define-fun .def_2017 () (_ BitVec 32) (bvshl .def_2000 (_ bv2 32)))
(define-fun .def_5373 () (_ BitVec 32) (bvadd pp .def_2017))
(define-fun .def_5374 () (_ BitVec 32) (|*(void)*@5| .def_5373))
(define-fun .def_9981 () Bool (= |main::b at 3| .def_5374))
(define-fun .def_10229 () Bool (and .def_9981 .def_10228))
(define-fun .def_7641 () Bool (= |g::i at 3| (_ bv2 32)))
(define-fun .def_7668 () Bool (not .def_7641))
(define-fun .def_10230 () Bool (and .def_7668 .def_10229))
(define-fun .def_7642 () Bool (= |g::i at 3| (_ bv1 32)))
(define-fun .def_7667 () Bool (not .def_7642))
(define-fun .def_10231 () Bool (and .def_7667 .def_10230))
(define-fun .def_371 () Bool (= |g::i at 3| (_ bv0 32)))
(define-fun .def_10232 () Bool (and .def_371 .def_10231))
(define-fun .def_7229 () Bool (= |g::pointer at 2| .def_1615))
(define-fun .def_10233 () Bool (and .def_7229 .def_10232))
(define-fun .def_5375 () (_ BitVec 32) (bvmul (_ bv4294967295 32) .def_5374))
(define-fun .def_5376 () (_ BitVec 32) (bvadd |g::pointer at 2| .def_5375))
(define-fun .def_5377 () Bool (= .def_5376 (_ bv4294967295 32)))
(define-fun .def_10234 () Bool (and .def_5377 .def_10233))
(define-fun .def_10235 () Bool (and .def_2706 .def_10234))
(define-fun .def_1992 () Bool (= .def_381 (_ bv0 32)))
(define-fun .def_10236 () Bool (and .def_1992 .def_10235))
(define-fun .def_1018 () (_ BitVec 32) (*int at 5 pstate))
(define-fun .def_1597 () Bool (= .def_1018 (_ bv1 32)))
(define-fun .def_10237 () Bool (and .def_1597 .def_10236))
(define-fun .def_395 () (_ BitVec 32) (bvadd pstate .def_381))
(define-fun .def_1591 () (_ BitVec 32) (*int at 5 .def_395))
(define-fun .def_1592 () Bool (= .def_1591 (_ bv1 32)))
(define-fun .def_10238 () Bool (and .def_1592 .def_10237))
(define-fun .def_1593 () (_ BitVec 32) (ite .def_1592 (_ bv1 32) (_ bv0 32)))
(define-fun .def_1594 () Bool (= .def_1593 (_ bv0 32)))
(define-fun .def_1621 () Bool (not .def_1594))
(define-fun .def_10239 () Bool (and .def_1621 .def_10238))
(define-fun .def_2002 () Bool (= .def_2000 |g::i at 4|))
(define-fun .def_1616 () Bool (= |g::__cil_tmp4 at 3| .def_1615))
(define-fun .def_379 () Bool (= |g::pointer at 2| |g::__cil_tmp3 at 3|))
(define-fun .def_1617 () Bool (and .def_379 .def_1616))
(define-fun .def_373 () Bool (bvslt |g::i at 3| (_ bv2 32)))
(define-fun .def_374 () (_ BitVec 32) (ite .def_373 (_ bv1 32) (_ bv0 32)))
(define-fun .def_375 () Bool (= .def_374 (_ bv0 32)))
(define-fun .def_376 () Bool (not .def_375))
(define-fun .def_1618 () Bool (and .def_376 .def_1617))
(define-fun .def_389 () Bool (= |g::__cil_tmp3 at 3| |g::__cil_tmp4 at 3|))
(define-fun .def_390 () (_ BitVec 32) (ite .def_389 (_ bv1 32) (_ bv0 32)))
(define-fun .def_391 () Bool (= .def_390 (_ bv0 32)))
(define-fun .def_1620 () Bool (and .def_391 .def_1618))
(define-fun .def_1242 () Bool (= .def_1018 .def_1241))
(define-fun .def_20 () (_ BitVec 32) (bvadd (_ bv4 32) pstate))
(define-fun .def_1236 () (_ BitVec 32) (*int at 6 .def_20))
(define-fun .def_1014 () (_ BitVec 32) (*int at 5 .def_20))
(define-fun .def_1237 () Bool (= .def_1014 .def_1236))
(define-fun .def_1454 () Bool (and .def_1237 .def_1242))
(define-fun .def_1997 () Bool (and .def_1454 .def_1620))
(define-fun .def_1993 () Bool (or .def_1242 .def_1992))
(define-fun .def_1989 () Bool (= .def_381 (_ bv4 32)))
(define-fun .def_1990 () Bool (or .def_1237 .def_1989))
(define-fun .def_1994 () Bool (and .def_1990 .def_1993))
(define-fun .def_1840 () (_ BitVec 32) (*int at 6 .def_395))
(define-fun .def_1987 () Bool (= .def_1840 (_ bv2 32)))
(define-fun .def_1995 () Bool (and .def_1987 .def_1994))
(define-fun .def_392 () Bool (not .def_391))
(define-fun .def_1619 () Bool (and .def_392 .def_1618))
(define-fun .def_1622 () Bool (and .def_1619 .def_1621))
(define-fun .def_1996 () Bool (and .def_1622 .def_1995))
(define-fun .def_1998 () Bool (or .def_1996 .def_1997))
(define-fun .def_2003 () Bool (and .def_1998 .def_2002))
(define-fun .def_23 () (_ BitVec 32) (bvadd (_ bv8 32) pp))
(define-fun .def_26 () Bool (bvslt pstate .def_23))
(define-fun .def_27 () Bool (not .def_26))
(define-fun .def_24 () Bool (bvslt (_ bv0 32) .def_23))
(define-fun .def_28 () Bool (and .def_24 .def_27))
(define-fun .def_15 () Bool (bvslt (_ bv0 32) pp))
(define-fun .def_29 () Bool (and .def_15 .def_28))
(define-fun .def_2004 () Bool (and .def_29 .def_2003))
(define-fun .def_10269 () Bool (and .def_2004 .def_10239))
(define-fun .def_10276 () Bool (and .def_10269 .def_10275))
(assert .def_10276)
(check-allsat (PRED13 PRED16 PRED17 PRED22 PRED26 PRED32))
-------- End of forwarded message --------

-- 
Best regards, Evgeny Novikov.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: segfault1.smt2
Type: application/octet-stream
Size: 10213 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130824/4271636d/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: segfault2.smt2
Type: application/octet-stream
Size: 20781 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130824/4271636d/attachment-0001.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: segfault3.smt2
Type: application/octet-stream
Size: 10332 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130824/4271636d/attachment-0002.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: segfault4.smt2
Type: application/octet-stream
Size: 10158 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130824/4271636d/attachment-0003.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: allsattimeout.smt2
Type: application/octet-stream
Size: 8909 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130824/4271636d/attachment-0004.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: abmixed1_segfault.smt2
Type: application/octet-stream
Size: 11560 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130824/4271636d/attachment-0005.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: hugeinterpolation_unknown.smt2
Type: application/octet-stream
Size: 11322 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130824/4271636d/attachment-0006.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: hugeinterpolant.smt2
Type: application/octet-stream
Size: 309316 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130824/4271636d/attachment-0007.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: justformula.smt2
Type: application/octet-stream
Size: 134282 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20130824/4271636d/attachment-0008.obj>