Open
Description
Describe the bug
An assertion failure in debug build with cadical as sat solver.
Output of ./bin/cvc5 -i --sat-solver=cadical temp.smt2
sat
Fatal failure within void cvc5::internal::SharedTermsDatabase::addSharedTerm(cvc5::internal::TNode, cvc5::internal::TNode, cvc5::internal::theory::TheoryIdSet) at /mnt/r/cvc5/src/theory/shared_terms_database.cpp:99
Check failure
theories != (*find).second
Aborted (core dumped)
Note: If the bug is triggered with an SMT2 input file please minimize it with ddsmt.
It is derived from test/regress/cli/regress1/strings/issue6072-inc-no-const-reg.smt2 which outputs the same error when I was debugging with my version of minisat with IPASIRUP interface. I constructed the temp.smt2 below which would also fail with cadical.
temp.smt2:
; COMMAND-LINE: -i
; EXPECT: sat
; EXPECT: sat
(set-logic ALL)
(declare-fun s () String)
;
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (or (not a) b))
(assert (or (not b) a))
(assert (or a b))
; This part above is to force `a` to be a fixed assignment at user level 1, so that the literal for `(= (str.len s) 0)` will be renotified and produce the error
(assert (or (not a) (= (str.len s) 0)))
(push)
(check-sat)
(pop)
(check-sat)Command line arguments: -i --sat-solver=cadical temp.smt2
cvc5 version/commit: commit e501c9b (grafted, HEAD -> main, tag: latest, origin/main, origin/HEAD)
Operating system: Ubuntu 22.04.2 LTS (wsl2)
configure.sh options
./configure.sh debug --auto-download
configure.sh output
-- The C compiler identification is GNU 11.4.0
-- The CXX compiler identification is GNU 11.4.0
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /usr/bin/cc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Found Git: /usr/bin/git (found version "2.34.1")
fatal: No names found, cannot describe anything.
-- Building Debug build
-- Performing Test HAVE_C_FLAG_fno_inline
-- Performing Test HAVE_C_FLAG_fno_inline - Success
-- Configuring with C flag '-fno-inline'
-- Performing Test HAVE_CXX_FLAG_fno_inline
-- Performing Test HAVE_CXX_FLAG_fno_inline - Success
-- Configuring with CXX flag '-fno-inline'
-- Performing Test HAVE_C_FLAG_Og
-- Performing Test HAVE_C_FLAG_Og - Success
-- Configuring with C flag '-Og'
-- Performing Test HAVE_CXX_FLAG_Og
-- Performing Test HAVE_CXX_FLAG_Og - Success
-- Configuring with CXX flag '-Og'
-- Performing Test HAVE_C_FLAG_Wall
-- Performing Test HAVE_C_FLAG_Wall - Success
-- Configuring with C flag '-Wall'
-- Performing Test HAVE_CXX_FLAG_Wall
-- Performing Test HAVE_CXX_FLAG_Wall - Success
-- Configuring with CXX flag '-Wall'
-- Performing Test HAVE_C_FLAG_Wunused_private_field
-- Performing Test HAVE_C_FLAG_Wunused_private_field - Failed
-- Performing Test HAVE_CXX_FLAG_Wunused_private_field
-- Performing Test HAVE_CXX_FLAG_Wunused_private_field - Failed
-- Performing Test HAVE_C_FLAG_Wdangling_reference
-- Performing Test HAVE_C_FLAG_Wdangling_reference - Failed
-- Performing Test HAVE_CXX_FLAG_Wdangling_reference
-- Performing Test HAVE_CXX_FLAG_Wdangling_reference - Failed
-- Performing Test HAVE_C_FLAG_fexceptions
-- Performing Test HAVE_C_FLAG_fexceptions - Success
-- Configuring with C flag '-fexceptions'
-- Performing Test HAVE_CXX_FLAG_Wsuggest_override
-- Performing Test HAVE_CXX_FLAG_Wsuggest_override - Success
-- Configuring with CXX flag '-Wsuggest-override'
-- Performing Test HAVE_CXX_FLAG_Wnon_virtual_dtor
-- Performing Test HAVE_CXX_FLAG_Wnon_virtual_dtor - Success
-- Configuring with CXX flag '-Wnon-virtual-dtor'
-- Performing Test HAVE_C_FLAG_Wimplicit_fallthrough
-- Performing Test HAVE_C_FLAG_Wimplicit_fallthrough - Success
-- Configuring with C flag '-Wimplicit-fallthrough'
-- Performing Test HAVE_CXX_FLAG_Wimplicit_fallthrough
-- Performing Test HAVE_CXX_FLAG_Wimplicit_fallthrough - Success
-- Configuring with CXX flag '-Wimplicit-fallthrough'
-- Performing Test HAVE_C_FLAG_Wshadow
-- Performing Test HAVE_C_FLAG_Wshadow - Success
-- Configuring with C flag '-Wshadow'
-- Performing Test HAVE_CXX_FLAG_Wshadow
-- Performing Test HAVE_CXX_FLAG_Wshadow - Success
-- Configuring with CXX flag '-Wshadow'
-- Performing Test HAVE_C_FLAG_fno_operator_names
-- Performing Test HAVE_C_FLAG_fno_operator_names - Failed
-- Performing Test HAVE_CXX_FLAG_fno_operator_names
-- Performing Test HAVE_CXX_FLAG_fno_operator_names - Success
-- Configuring with CXX flag '-fno-operator-names'
-- Performing Test HAVE_CXX_FLAG_fno_extern_tls_init
-- Performing Test HAVE_CXX_FLAG_fno_extern_tls_init - Success
-- Configuring with CXX flag '-fno-extern-tls-init'
-- Performing Test HAVE_CXX_FLAG_Wclass_memaccess
-- Performing Test HAVE_CXX_FLAG_Wclass_memaccess - Success
-- Configuring with CXX flag '-Wno-class-memaccess'
-- Using GNU gold linker.
-- Performing Test HAVE_CXX_FLAGfaccess_control
-- Performing Test HAVE_CXX_FLAGfaccess_control - Success
-- Found Python: /usr/bin/python3 (found version "3.10.12") found components: Interpreter
-- Found Python: /mnt/r/cvc5/build/venv-3.10.12/bin/python3 (found version "3.10.12") found components: Interpreter
-- Found GMP 6.2.1: /usr/lib/x86_64-linux-gnu/libgmp.so
-- Performing Test HAVE_C_FLAG_ggdb3
-- Performing Test HAVE_C_FLAG_ggdb3 - Success
-- Configuring with C flag '-ggdb3'
-- Performing Test HAVE_CXX_FLAG_ggdb3
-- Performing Test HAVE_CXX_FLAG_ggdb3 - Success
-- Configuring with CXX flag '-ggdb3'
-- Performing Test HAVE_C_FLAG_gz
-- Performing Test HAVE_C_FLAG_gz - Success
-- Configuring with C flag '-gz'
-- Performing Test HAVE_CXX_FLAG_gz
-- Performing Test HAVE_CXX_FLAG_gz - Success
-- Configuring with CXX flag '-gz'
-- Looking for getc_unlocked
-- Looking for getc_unlocked - not found
-- Looking for closefrom
-- Looking for closefrom - not found
-- Building CaDiCaL rel-2.1.3: /mnt/r/cvc5/build/deps/lib/libcadical.a
-- Building Poly 0.2.0: /mnt/r/cvc5/build/deps/lib/libpoly.so, /mnt/r/cvc5/build/deps/lib/libpolyxx.so
-- Building SymFPU: /mnt/r/cvc5/build/deps/include/
-- Performing Test CVC5_NEED_INT64_T_OVERLOADS
-- Performing Test CVC5_NEED_INT64_T_OVERLOADS - Failed
-- Performing Test CVC5_NEED_HASH_UINT64_T_OVERLOAD
-- Performing Test CVC5_NEED_HASH_UINT64_T_OVERLOAD - Failed
-- Looking for unistd.h
-- Looking for unistd.h - found
-- Looking for sys/wait.h
-- Looking for sys/wait.h - found
-- Looking for C++ include ext/stdio_filebuf.h
-- Looking for C++ include ext/stdio_filebuf.h - found
-- Looking for clock_gettime
-- Looking for clock_gettime - found
-- Looking for ffs
-- Looking for ffs - found
-- Looking for optreset
-- Looking for optreset - not found
-- Looking for sigaltstack
-- Looking for sigaltstack - found
-- Looking for strerror_r
-- Looking for strerror_r - found
-- Looking for strtok_r
-- Looking for strtok_r - found
-- Looking for setitimer
-- Looking for setitimer - found
-- Performing Test STRERROR_R_CHAR_P
-- Performing Test STRERROR_R_CHAR_P - Failed
-- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY
-- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY - Success
-- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY
-- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY - Success
-- Performing Test COMPILER_HAS_DEPRECATED_ATTR
-- Performing Test COMPILER_HAS_DEPRECATED_ATTR - Success
-- Building GTest 1.11.0: /mnt/r/cvc5/build/deps/lib/libgtest.a
-- Performing Test HAVE_CXX_FLAGWunused_comparison
-- Performing Test HAVE_CXX_FLAGWunused_comparison - Failed
cvc5 1.2.1
Build profile : debug
Assertions : on
Debug symbols : on
Debug context mem mgr : off
Muzzle : off
Statistics : on
Tracing : on
ASan : off
UBSan : off
TSan : off
Coverage (gcov) : off
Profiling (gprof) : off
Unit tests : on
Valgrind : off
Shared build : on
Python bindings : off
Java bindings : off
Interprocedural opt. : off
CryptoMiniSat : off
GLPK : off
Kissat : off
LibPoly : on (local)
CoCoALib : off
MP library : gmp (system)
Editline : off
Api docs : off
CPPLAGS (-D...): CVC5_DEBUG CVC5_ASSERTIONS CVC5_TRACING CVC5_STATISTICS_ON CVC5_USE_POLY
CXXFLAGS : -fno-inline -Og -Wall -Wsuggest-override -Wnon-virtual-dtor -Wimplicit-fallthrough -Wshadow -fno-operator-names -fno-extern-tls-init -Wno-class-memaccess -ggdb3 -gz
CFLAGS : -fno-inline -Og -Wall -fexceptions -Wimplicit-fallthrough -Wshadow -ggdb3 -gz
Linker flags : -fuse-ld=gold
Install prefix : /usr/local
cvc5 license: modified BSD
Note that this configuration is NOT built against any GPL'ed libraries, so
it is covered by the (modified) BSD license. To build against GPL'ed
libraries which can improve cvc5's performance on arithmetic and bit-vector
logics, use the 'configure.sh' script to re-configure with '--best --gpl'.
Now change to 'build' and type 'make', followed by 'make check' or 'make install'.
-- Configuring done
-- Generating done
-- Build files have been written to: /mnt/r/cvc5/build