Skip to content

Why does the divide by 0 error crash? #10813

Closed
@Heaven2024

Description

@Heaven2024

Hi!
this commit is cvc5 1.1.3-dev.282.2b8054af5 [git 2b8054a on branch main]
ubuntu:22.04
Why does the following example crash? Generally speaking, shouldn't it return a parsing error?

cvc5  small.smt2
info:
AddressSanitizer:DEADLYSIGNAL
=================================================================
==2711627==ERROR: AddressSanitizer: FPE on unknown address 0x00000029604b (pc 0x7ffff1db39fc bp 0x00000029604b sp 0x7fffffffc8b0 T0)
    #0 0x7ffff1db39fc in pthread_kill (/usr/lib/x86_64-linux-gnu/libc.so.6+0x969fc) (BuildId: 962015aa9d133c6cbcfb31ec300596d7f44d3348)
    #1 0x7ffff1d5f475 in gsignal (/usr/lib/x86_64-linux-gnu/libc.so.6+0x42475) (BuildId: 962015aa9d133c6cbcfb31ec300596d7f44d3348)
    #2 0x7ffff1bfca0c in __gmp_exception (/usr/lib/x86_64-linux-gnu/libgmp.so.10+0xaa0c) (BuildId: f110719303ddbea25a5e89ff730fec520eed67b0)
    #3 0x7ffff1bfca53 in __gmp_divide_by_zero (/usr/lib/x86_64-linux-gnu/libgmp.so.10+0xaa53) (BuildId: f110719303ddbea25a5e89ff730fec520eed67b0)
    #4 0x7ffff1c1afb4 in __gmpq_canonicalize (/usr/lib/x86_64-linux-gnu/libgmp.so.10+0x28fb4) (BuildId: f110719303ddbea25a5e89ff730fec520eed67b0)
    #5 0x7ffff2696369 in __gmp_expr<__mpq_struct [1], __mpq_struct [1]>::canonicalize() /usr/include/gmpxx.h:1785:25
    #6 0x7ffff2696369 in cvc5::internal::Rational::Rational(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>> const&, unsigned int) /yuhao/cvc5/src/./util/rational_gmp_imp.h:81:13
    #7 0x7ffff2696369 in cvc5::TermManager::mkRealOrIntegerFromStrHelper(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>> const&, bool) /yuhao/cvc5/src/api/cpp/cvc5.cpp:5376:34
    #8 0x7ffff26e7e73 in cvc5::TermManager::mkReal(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>> const&) /yuhao/cvc5/src/api/cpp/cvc5.cpp:6098:10
    #9 0x7ffff7eb7543 in cvc5::parser::Smt2TermParser::parseTerm() /yuhao/cvc5/src/parser/smt2/smt2_term_parser.cpp:287:18
    #10 0x7ffff7e8e150 in cvc5::parser::Smt2CmdParser::parseNextCommand() /yuhao/cvc5/src/parser/smt2/smt2_cmd_parser.cpp:133:26
    #11 0x7ffff7eb3c6d in cvc5::parser::Smt2Parser::parseNextCommand() /yuhao/cvc5/src/parser/smt2/smt2_parser.cpp:41:22
    #12 0x7ffff7de02ac in cvc5::parser::Parser::nextCommand() /yuhao/cvc5/src/parser/parser.cpp:75:11
    #13 0x7ffff7f48e13 in cvc5::parser::InputParser::nextCommand() /yuhao/cvc5/src/api/cpp/cvc5_parser.cpp:277:40
    #14 0x555555690f72 in cvc5::main::ExecutionContext::solveContinuous(cvc5::parser::InputParser*, bool) /yuhao/cvc5/src/main/portfolio_driver.cpp:60:19
    #15 0x55555569379f in cvc5::main::PortfolioDriver::solve(std::unique_ptr<cvc5::main::CommandExecutor, std::default_delete<cvc5::main::CommandExecutor>>&) /yuhao/cvc5/src/main/portfolio_driver.cpp
    #16 0x55555566eb8d in runCvc5(int, char**, std::unique_ptr<cvc5::Solver, std::default_delete<cvc5::Solver>>&) /yuhao/cvc5/src/main/driver_unified.cpp:242:28
    #17 0x55555567592d in main /yuhao/cvc5/src/main/main.cpp:37:12
    #18 0x7ffff1d46d8f  (/usr/lib/x86_64-linux-gnu/libc.so.6+0x29d8f) (BuildId: 962015aa9d133c6cbcfb31ec300596d7f44d3348)
    #19 0x7ffff1d46e3f in __libc_start_main (/usr/lib/x86_64-linux-gnu/libc.so.6+0x29e3f) (BuildId: 962015aa9d133c6cbcfb31ec300596d7f44d3348)
    #20 0x555555591564 in _start (/yuhao/cvc5/build/bin/cvc5+0x3d564) (BuildId: 78dc0d78a1cc9d2f164839f1bfd99a1b79a286c0)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: FPE (/usr/lib/x86_64-linux-gnu/libc.so.6+0x969fc) (BuildId: 962015aa9d133c6cbcfb31ec300596d7f44d3348) in pthread_kill
==2711627==ABORTING

cat small.smt2
(set-logic QF_LRA)
(declare-const x Real)
(declare-const y Real)
(assert (> x 1.5))
(assert (< y 3.5))
(assert (= (+ x y) 5/0))
(check-sat)

Is this a bug? Hope to get your answer. Thanks:)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions