search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
368 stars 46 forks source link

Assertion failed: ((d->len == 1 && d->prod[0].exp == 2) || (d->len == 2 && d->prod[0].exp == 1 && d->prod[1].exp == 1)), function bvc_process_elem_prod #273

Closed dddejan closed 4 years ago

dddejan commented 4 years ago

For the following problem 

(set-logic QF_BV)
(declare-fun x () (_ BitVec 28))
(declare-fun b1 () Bool)
(declare-fun b2 () Bool)
(declare-fun b3 () Bool)
(declare-fun b4 () Bool)
(declare-fun b5 () Bool)
(declare-fun b6 () Bool)
(declare-fun b7 () Bool)
(declare-fun b8 () Bool)
(declare-fun b9 () Bool)
(declare-fun b10 () Bool)
(declare-fun b11 () Bool)
(declare-fun b12 () Bool)
(declare-fun v0 () (_ BitVec 12))
(declare-fun v2 () (_ BitVec 13))
(declare-fun v4 () (_ BitVec 22))
(assert
  (let ((e42 (bvmul (ite (bvsge v4 (_ bv0 22)) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 15) v2) x) (_ bv1 1) (_ bv0 1)))))
  (let ((e524 (not (=> (not (= ((_ sign_extend 12) e42) (bvnand (_ bv0 13) (_ bv0 13)))) b12)))) (and (and (and (and (and (and (and (and (and (and (= (xor (bvsge (_ bv0 13) v2) (not (or (not (= ((_ zero_extend 2) v0) (bvmul ((_ zero_extend 13) e42) ((_ sign_extend 13) e42)))) b1))) (not (=> (not (= ((_ sign_extend 12) e42) (bvnand (_ bv0 13) (_ bv0 13)))) b12))) b6) b7) b2) b8) b3) b4) b5) b9) b10) b11))))
(check-sat)

We currently get 

$ ./yices_smt2 --mcsat --trace mcsat::conflict::check issue.smt2 
Assertion failed: ((d->len == 1 && d->prod[0].exp == 2) || (d->len == 2 && d->prod[0].exp == 1 && d->prod[1].exp == 1)), function bvc_process_elem_prod, file solvers/bv/bvpoly_compiler.c, line 1002.

The backtrace

* thread #1, queue = 'com.apple.main-thread', stop reason = signal SIGABRT
  * frame #0: 0x00007fff6a1d033a libsystem_kernel.dylib`__pthread_kill + 10
    frame #1: 0x00007fff6a28ce60 libsystem_pthread.dylib`pthread_kill + 430
    frame #2: 0x00007fff6a157808 libsystem_c.dylib`abort + 120
    frame #3: 0x00007fff6a156ac6 libsystem_c.dylib`__assert_rtn + 314
    frame #4: 0x00000001000d5774 yices_smt2`bvc_process_elem_prod(c=0x00000001009224f0, i=5, d=0x0000000101856b30) at bvpoly_compiler.c:1001:3
    frame #5: 0x00000001000d50b9 yices_smt2`bvc_process_elem_node(c=0x00000001009224f0, i=5) at bvpoly_compiler.c:1113:5
    frame #6: 0x00000001000d34ac yices_smt2`bv_compiler_convert_elem_nodes(c=0x00000001009224f0) at bvpoly_compiler.c:1333:5
    frame #7: 0x00000001000d2e48 yices_smt2`bv_compiler_process_queue(c=0x00000001009224f0) at bvpoly_compiler.c:1473:5
    frame #8: 0x00000001000e401d yices_smt2`bv_solver_compile_polynomials(solver=0x000000010091c930) at bvsolver.c:1038:3
    frame #9: 0x00000001000e3c69 yices_smt2`bv_solver_bitblast(solver=0x000000010091c930) at bvsolver.c:1951:3
    frame #10: 0x00000001000eb48d yices_smt2`bv_solver_start_search(solver=0x000000010091c930) at bvsolver.c:7134:14
    frame #11: 0x0000000100141946 yices_smt2`egraph_start_search(egraph=0x0000000101841e00) at egraph.c:4481:7
    frame #12: 0x000000010012caaf yices_smt2`start_search(s=0x0000000100916ab0, n=0, a=0x0000000000000000) at smt_core.c:5915:3
    frame #13: 0x0000000100043bb7 yices_smt2`solve(core=0x0000000100916ab0, params=0x00007ffeefbfeee0, n=0, a=0x0000000000000000) at context_solver.c:396:3
    frame #14: 0x00000001000437da yices_smt2`check_context(ctx=0x000000010183c410, params=0x00007ffeefbfeee0) at context_solver.c:582:5
    frame #15: 0x000000010001470b yices_smt2`yices_check_context(ctx=0x000000010183c410, params=0x00007ffeefbfeee0) at yices_api.c:8869:12
    frame #16: 0x000000010025b2a3 yices_smt2`conflict_check(conflict=0x00007ffeefbff090) at conflict.c:52:25
    frame #17: 0x0000000100252667 yices_smt2`mcsat_analyze_conflicts(mcsat=0x0000000101813a00, restart_resource=0x00007ffeefbff39c) at solver.c:1726:7
    frame #18: 0x00000001002511f7 yices_smt2`mcsat_solve(mcsat=0x0000000101813a00, params=0x000000010033fb28) at solver.c:2191:5
    frame #19: 0x0000000100045461 yices_smt2`_o_call_mcsat_solver(ctx=0x0000000101813010, params=0x000000010033fb28) at context_solver.c:552:3
    frame #20: 0x000000010004381d yices_smt2`call_mcsat_solver(ctx=0x0000000101813010, params=0x000000010033fb28) at context_solver.c:557:3
    frame #21: 0x0000000100043790 yices_smt2`check_context(ctx=0x0000000101813010, params=0x000000010033fb28) at context_solver.c:574:12
    frame #22: 0x00000001002d41d5 yices_smt2`check_sat_with_timeout(g=0x000000010033fa50, params=0x000000010033fb28) at smt2_commands.c:2551:12
    frame #23: 0x00000001002ce421 yices_smt2`check_delayed_assertions(g=0x000000010033fa50) at smt2_commands.c:2931:11
    frame #24: 0x00000001002cddeb yices_smt2`smt2_check_sat at smt2_commands.c:6127:9
    frame #25: 0x00000001002df6e8 yices_smt2`eval_smt2_check_sat(stack=0x000000010033eaf8, f=0x0000000101808a40, n=0) at smt2_term_stack.c:1037:3
    frame #26: 0x00000001000b848e yices_smt2`tstack_eval(stack=0x000000010033eaf8) at term_stack2.c:5447:5
    frame #27: 0x00000001002d9298 yices_smt2`smt2_parse(parser=0x000000010033ec60, start=c0) at smt2_parser.c:306:7
    frame #28: 0x00000001002d8be7 yices_smt2`parse_smt2_command(parser=0x000000010033ec60) at smt2_parser.c:927:10
    frame #29: 0x0000000100001345 yices_smt2`main(argc=5, argv=0x00007ffeefbff8a8) at yices_smt2.c:739:12
    frame #30: 0x00007fff6a088cc9 libdyld.dylib`start + 1
    frame #31: 0x00007fff6a088cc9 libdyld.dylib`start + 1
BrunoDutertre commented 4 years ago

Fixed by 3f56e172d4c6aa7b050fcc47ef10c38897b65587.