search

cvc5 / cvc5-projects

1 stars 0 forks source link

Segment fault on QF_LIA formula (use-soi) #201

Closed rainoftime closed 3 years ago

rainoftime commented 4 years ago 
(set-logic QF_LIA)
(set-option :use-soi true)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const i2 Int)
(declare-const i4 Int)
(declare-const v13 Bool)
(declare-const v37 Bool)
(assert (or v13 (distinct v2 (xor false (<= i4 i2)) v37 false v3 v1)))
(check-sat)

cvc4 commit 61734b4 throws a segfault (The category of use-soi is "regular")

ASAN:SIGSEGV
=================================================================
==98335==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x7fe7992a9c73 bp 0x7ffc794363c0 sp 0x7ffc79435e90 T0)
    #0 0x7fe7992a9c72 in CVC4::theory::arith::SumOfInfeasibilitiesSPD::selectUpdate(bool (CVC4::theory::arith::LinearEqualityModule::*)(CVC4::theory::arith::UpdateInfo const&, CVC4::theory::arith::UpdateI
nfo const&) const, unsigned int (CVC4::theory::arith::LinearEqualityModule::*)(unsigned int, unsigned int) const) /home/peisen/test/tofuzz/CVC4/src/theory/arith/soi_simplex.cpp:303
    #1 0x7fe7992c2a2d in CVC4::theory::arith::SumOfInfeasibilitiesSPD::soiRound() /home/peisen/test/tofuzz/CVC4/src/theory/arith/soi_simplex.cpp:908
    #2 0x7fe7992c5153 in CVC4::theory::arith::SumOfInfeasibilitiesSPD::sumOfInfeasibilities() /home/peisen/test/tofuzz/CVC4/src/theory/arith/soi_simplex.cpp:981
    #3 0x7fe7992a4c38 in CVC4::theory::arith::SumOfInfeasibilitiesSPD::findModel(bool) /home/peisen/test/tofuzz/CVC4/src/theory/arith/soi_simplex.cpp:151
    #4 0x7fe79935f84f in CVC4::theory::arith::TheoryArithPrivate::solveRealRelaxation(CVC4::theory::Theory::Effort) /home/peisen/test/tofuzz/CVC4/src/theory/arith/theory_arith_private.cpp:3502
    #5 0x7fe7993650cc in CVC4::theory::arith::TheoryArithPrivate::check(CVC4::theory::Theory::Effort) /home/peisen/test/tofuzz/CVC4/src/theory/arith/theory_arith_private.cpp:3816
    #6 0x7fe7992e43b2 in CVC4::theory::arith::TheoryArith::check(CVC4::theory::Theory::Effort) /home/peisen/test/tofuzz/CVC4/src/theory/arith/theory_arith.cpp:106
    #7 0x7fe79ab40da6 in CVC4::TheoryEngine::check(CVC4::theory::Theory::Effort) /home/peisen/test/tofuzz/CVC4/src/theory/theory_engine.cpp:606
    #8 0x7fe798c58a45 in CVC4::prop::TheoryProxy::theoryCheck(CVC4::theory::Theory::Effort) /home/peisen/test/tofuzz/CVC4/src/prop/theory_proxy.cpp:62
    #9 0x7fe798b90228 in CVC4::Minisat::Solver::theoryCheck(CVC4::theory::Theory::Effort) /home/peisen/test/tofuzz/CVC4/src/prop/minisat/core/Solver.cc:1190
    #10 0x7fe798b8e0ed in CVC4::Minisat::Solver::propagate(CVC4::Minisat::Solver::TheoryCheckType) /home/peisen/test/tofuzz/CVC4/src/prop/minisat/core/Solver.cc:1104
    #11 0x7fe798b9623c in CVC4::Minisat::Solver::search(int) /home/peisen/test/tofuzz/CVC4/src/prop/minisat/core/Solver.cc:1407
    #12 0x7fe798b9d25f in CVC4::Minisat::Solver::solve_() /home/peisen/test/tofuzz/CVC4/src/prop/minisat/core/Solver.cc:1627
    #13 0x7fe798c1e799 in CVC4::Minisat::SimpSolver::solve_(bool, bool) /home/peisen/test/tofuzz/CVC4/src/prop/minisat/simp/SimpSolver.cc:148
    #14 0x7fe798c15bd9 in CVC4::Minisat::SimpSolver::solve(bool, bool) /home/peisen/test/tofuzz/CVC4/src/./prop/minisat/simp/SimpSolver.h:201
    #15 0x7fe798c0dd3c in CVC4::prop::MinisatSatSolver::solve() /home/peisen/test/tofuzz/CVC4/src/prop/minisat/minisat.cpp:185
    #16 0x7fe798c46216 in CVC4::prop::PropEngine::checkSat() /home/peisen/test/tofuzz/CVC4/src/prop/prop_engine.cpp:198
    #17 0x7fe798d4723e in CVC4::SmtEngine::check() /home/peisen/test/tofuzz/CVC4/src/smt/smt_engine.cpp:1385
    #18 0x7fe798d4eafa in CVC4::SmtEngine::checkSatisfiability(std::vector<CVC4::Expr, std::allocator<CVC4::Expr> > const&, bool, bool) /home/peisen/test/tofuzz/CVC4/src/smt/smt_engine.cpp:1691
    #19 0x7fe798d4d294 in CVC4::SmtEngine::checkSatisfiability(CVC4::Expr const&, bool, bool) /home/peisen/test/tofuzz/CVC4/src/smt/smt_engine.cpp:1604
    #20 0x7fe798d4bf84 in CVC4::SmtEngine::checkSat(CVC4::Expr const&, bool) /home/peisen/test/tofuzz/CVC4/src/smt/smt_engine.cpp:1565
    #21 0x7fe798c6ea41 in CVC4::CheckSatCommand::invoke(CVC4::SmtEngine*) /home/peisen/test/tofuzz/CVC4/src/smt/command.cpp:386
    #22 0x7fe798c68bd5 in CVC4::Command::invoke(CVC4::SmtEngine*, std::ostream&) /home/peisen/test/tofuzz/CVC4/src/smt/command.cpp:174
    #23 0x440111 in CVC4::main::smtEngineInvoke(CVC4::SmtEngine*, CVC4::Command*, std::ostream*) /home/peisen/test/tofuzz/CVC4/src/main/command_executor.cpp:205
    #24 0x43d3bf in CVC4::main::CommandExecutor::doCommandSingleton(CVC4::Command*) /home/peisen/test/tofuzz/CVC4/src/main/command_executor.cpp:121
    #25 0x43c6a1 in CVC4::main::CommandExecutor::doCommand(CVC4::Command*) /home/peisen/test/tofuzz/CVC4/src/main/command_executor.cpp:98
    #26 0x4268a1 in runCvc4(int, char**, CVC4::Options&) /home/peisen/test/tofuzz/CVC4/src/main/driver_unified.cpp:446
rainoftime commented 4 years ago

Seems the option is not on the list https://github.com/CVC4/CVC4/wiki/Fuzzing-CVC4. Maybe the soi procedure is deprecated?

ajreynol commented 3 years ago

Does not occur on https://github.com/cvc5/cvc5/commit/a517a9127e0ef70424364d093bb21be64891dd0d.