hifrog

/hifrog --claim 1 --theoref ~/dev/hi-bench/challenge-bench/sv-comp16/c/ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c

Parts of debug:
...
....
; Warning: disabling SATElite preprocessing to track proof
^C^C
Program received signal SIGINT, Interrupt.
0x00000000005c300a in operator!= (a1=..., a2=...)
at /home/asadis/dev/opensmt-debug/include/opensmt/Pterm.h:43
43 inline friend bool operator!= (const PTRef& a1, const PTRef& a2) { return a1.x != a2.x; }
(gdb) bt
#0 0x00000000005c300a in operator!= (a1=..., a2=...)
at /home/asadis/dev/opensmt-debug/include/opensmt/Pterm.h:43
#1 0x00007ffff7acc7f4 in operator== (k1=..., k2=...) at ../../src/pterms/Pterm.h:69
#2 0x00007ffff7ad0e01 in Equal<PTLKey>::operator() (this=0x1d53ae9, k1=..., k2=...)
at ../../src/minisat/mtl/Map.h:32
#3 0x00007ffff7ace677 in Map<PTLKey, PTRef, PTLHash, Equal<PTLKey> >::has (
this=0x1d53ae8, k=...) at ../../src/minisat/mtl/Map.h:149
#4 0x00007ffff7accece in PtStore::hasBoolKey (this=0x1d539c0, k=...)
at ../../src/pterms/PtStore.h:175
#5 0x00007ffff7ac5acf in Logic::insertTermHash (this=0x1d53708, sym=..., terms_in=...)
at Logic.C:1111
#6 0x00007ffff7ac44e7 in Logic::mkEq (this=0x1d53708, args=...) at Logic.C:831
#7 0x00000000005ccaf2 in Logic::mkEq (this=0x1d53708, a1=..., a2=...)
at /home/asadis/dev/opensmt-debug/include/opensmt/Logic.h:279
#8 0x00007ffff7aec8e8 in BVLogic::mkEq (this=0x1d53708, a1=..., a2=...) at BVLogic.h:274
#9 0x00007ffff7a7b942 in BitBlaster::notifyEquality (this=0x1e93410, tr=...)
at BitBlaster.C:2202
#10 0x00007ffff7a7b449 in BitBlaster::notifyEqualities (this=0x1e93410)
at BitBlaster.C:2162
#11 0x00000000005db719 in smtcheck_opensmt2t_cuf::refine_ce_mul (this=0x1e647e0,
exprs=std::vector of length 2594, capacity 4096 = {...},
is=std::set with 1184 elements = {...}) at solvers/smtcheck_opensmt2_cuf.cpp:1442
#12 0x00000000005a58e1 in theory_refinert::assertion_holds_smt (this=0x7fffffffd2c0,
assertion=..., store_summaries_with_assertion=true) at theory_refiner.cpp:178
#13 0x0000000000576027 in check_claims (ns=..., leaping_program=..., goto_functions=...,
claim_map=std::map with 1 elements = {...},
claim_numbers=std::map with 2 elements = {...}, options=..., _message_handler=...,
claim_nr=1) at check_claims.cpp:177
#14 0x0000000000570cf2 in funfrog_parseoptionst::check_function_summarization (
this=0x7fffffffdd90, ns=..., goto_functions=...) at parseoptions.cpp:541
#15 0x0000000000570395 in funfrog_parseoptionst::doit (this=0x7fffffffdd90)
---Type <return> to continue, or q <return> to quit---q
at parseoptionQuit
(gdb) f 9
....
...
main reason for this bug:
Theory combination between BV and CUF

need to be added millions of equalities in binding, indicating that qfcuf holds if and only if BV holds.