Boolector error involving constant array assignments

[dbueno]

Attached is a btor trace that leads to an error.
btor.trace.zip

I generated this trace when solving problems involving constant arrays. I am not sure what is going wrong but I hope it will be clear to the authors. Is this behavior expected or not?

[mpreiner]

What version of Boolector are you using and what error message do you get?

[dbueno]

Sorry about that. I'm using commit 62f1ec9 and the error message is:
0 | 21:00 $ ./bin/btoruntrace ~/Downloads/btor.trace
btoruntrace: expected return value 6 but got 10

[mpreiner]

Is this the original trace, which was also generated with the Boolector binary from commit 62f1ec9? Did you use Boolector via the API or did you provide an input file? In case of an input file, can you share it?

[dbueno]

I re-generated the trace to be sure that it was generated from commit 62f1ec9. It is attached. btor-62f1ec9.trace.zip The error now is:
1 | 11:26 $ ~/code/boolector3/build/bin/btoruntrace foo.trace
btoruntrace: expected return value 3 but got 10

I am calling Boolector using the API so there is no input file to share. :/

[mpreiner]

Hmm, can you configure Boolector with --asan -g and check if there is a memory issue and/or an assertion fails?

[dbueno]

For some reason, configuring with --asan -g forces dynamic libraries to be built, even if -DBUILD_SHARED_LIBS=OFF is set. (Right now I link Boolector in statically with my code.) But I configured without --asan instead and got an assertion failure. Here is the stack trace:

Assertion failed: (arity > 0), function btor_bv_new_tuple, file /Users/dbueno/code/boolector3/src/btorbv.c, line 3047.
Process 78989 stopped
* thread #1, queue = 'com.apple.main-thread', stop reason = signal SIGABRT
    frame #0: 0x00007fff5c622b66 libsystem_kernel.dylib`__pthread_kill + 10
libsystem_kernel.dylib`__pthread_kill:
->  0x7fff5c622b66 <+10>: jae    0x7fff5c622b70            ; <+20>
    0x7fff5c622b68 <+12>: movq   %rax, %rdi
    0x7fff5c622b6b <+15>: jmp    0x7fff5c619ae5            ; cerror_nocancel
    0x7fff5c622b70 <+20>: retq   
Target 0: (euforia) stopped.
(lldb) bt
* thread #1, queue = 'com.apple.main-thread', stop reason = signal SIGABRT
  * frame #0: 0x00007fff5c622b66 libsystem_kernel.dylib`__pthread_kill + 10
    frame #1: 0x00007fff5c7ed080 libsystem_pthread.dylib`pthread_kill + 333
    frame #2: 0x00007fff5c57e1ae libsystem_c.dylib`abort + 127
    frame #3: 0x00007fff5c5461ac libsystem_c.dylib`__assert_rtn + 320
    frame #4: 0x00000001001919e9 euforia`btor_bv_new_tuple(mm=0x0000000104a32a70, arity=0) at btorbv.c:3047
    frame #5: 0x00000001001e0fe1 euforia`recursively_compute_function_model(btor=0x0000000105848e00, bv_model=0x0000000104ac0620, fun_model=0x00000001090d0070, fun=0x0000000104f0a380) at btormodel.c:325
    frame #6: 0x00000001001ea77e euforia`compute_model_values(btor=0x0000000105848e00, bv_model=0x0000000104ac0620, fun_model=0x00000001090d0070, nodes=0x000000010585f600, num_nodes=962) at btormodel.c:494
    frame #7: 0x00000001001e980d euforia`btor_model_generate(btor=0x0000000105848e00, bv_model=0x0000000104ac0620, fun_model=0x00000001090d0070, model_for_all_nodes=true) at btormodel.c:1287
    frame #8: 0x000000010024322c euforia`generate_model_fun_solver(slv=0x0000000107725e60, model_for_all_nodes=true, reset=true) at btorslvfun.c:2609
    frame #9: 0x00000001001c7d2d euforia`btor_check_sat(btor=0x0000000105848e00, lod_limit=-1, sat_limit=-1) at btorcore.c:3052
    frame #10: 0x000000010012d868 euforia`boolector_sat(btor=0x0000000105848e00) at boolector.c:639
[snip]
(lldb) up
frame #1: 0x00007fff5c7ed080 libsystem_pthread.dylib`pthread_kill + 333
libsystem_pthread.dylib`pthread_kill:
    0x7fff5c7ed080 <+333>: movl   %eax, %r15d
    0x7fff5c7ed083 <+336>: cmpl   $-0x1, %r15d
    0x7fff5c7ed087 <+340>: jne    0x7fff5c7ed091            ; <+350>
    0x7fff5c7ed089 <+342>: callq  0x7fff5c7f012c            ; symbol stub for: __error
(lldb) 
frame #2: 0x00007fff5c57e1ae libsystem_c.dylib`abort + 127
libsystem_c.dylib`abort:
    0x7fff5c57e1ae <+127>: movl   $0x2710, %edi             ; imm = 0x2710 
    0x7fff5c57e1b3 <+132>: callq  0x7fff5c550728            ; usleep$NOCANCEL
    0x7fff5c57e1b8 <+137>: callq  0x7fff5c57e1bd            ; __abort

libsystem_c.dylib`__abort:
    0x7fff5c57e1bd <+0>:   cmpq   $0x0, 0x38960fa3(%rip)    ; gCRAnnotations + 7
(lldb) 
frame #3: 0x00007fff5c5461ac libsystem_c.dylib`__assert_rtn + 320
libsystem_c.dylib`basename_r:
    0x7fff5c5461ac <+0>: pushq  %rbp
    0x7fff5c5461ad <+1>: movq   %rsp, %rbp
    0x7fff5c5461b0 <+4>: pushq  %r15
    0x7fff5c5461b2 <+6>: pushq  %r14
(lldb) 
frame #4: 0x00000001001919e9 euforia`btor_bv_new_tuple(mm=0x0000000104a32a70, arity=0) at btorbv.c:3047
   3044 btor_bv_new_tuple (BtorMemMgr *mm, uint32_t arity)
   3045 {
   3046   assert (mm);
-> 3047   assert (arity > 0);
   3048
   3049   BtorBitVectorTuple *res = 0;
   3050

[mpreiner]

Ok that's the same assertion error I get on my machine. I'll take a look. Thanks for the infos!

[mpreiner]

@dbueno I've added new API checks and removed an incorrect assertion. Can you try again with latest master?

[dbueno]

I updated boolector to 4a3d82c. From this commit, I generated a new trace that produces an error. btor-4a3d82c.trace.zip

1 | 13:12 $ ~/code/boolector3/build/bin/btoruntrace btor-62f1ec9.trace
btoruntrace: expected return value 3 but got 10

The trace from 62f1ec9 also produces an error but I'm not sure if that's what you expect.

[mpreiner]

What happens if you run btoruntrace with option -s ?

[mpreiner]

What SAT solver do you use? Lingeling or CaDiCaL?

[dbueno]

1 | 13:22 $ ~/code/boolector3/build/bin/btoruntrace -s btor-62f1ec9.trace
AddressSanitizer:DEADLYSIGNAL
=================================================================
==14432==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x000101a59114 bp 0x7ffeee2b3d50 sp 0x7ffeee2b39c0 T0)
==14432==The signal is caused by a READ memory access.
==14432==Hint: address points to the zero page.
    #0 0x101a59113 in generate_fun_model_str boolector.c:4078
    #1 0x101a4c93d in fun_assignment boolector.c:4116
    #2 0x101a4b0ca in boolector_array_assignment boolector.c:4158
    #3 0x1019572af in parse btoruntrace.c:1754
    #4 0x10195dfda in main btoruntrace.c:2094
    #5 0x7fff5c4d2014 in start (libdyld.dylib:x86_64+0x1014)

==14432==Register values:
rax = 0x0000000000000000  rbx = 0x00007ffeee2b3a60  rcx = 0x0000602000413398  rdx = 0x0000000000000000  
rdi = 0x0000603000002b90  rsi = 0x0000100000000000  rbp = 0x00007ffeee2b3d50  rsp = 0x00007ffeee2b39c0  
 r8 = 0x00001fffddc56700   r9 = 0x00007ffeee2b39f8  r10 = 0x00000fffffffffff  r11 = 0xffffffffffffffff  
r12 = 0x0000000000000000  r13 = 0x0000000000000000  r14 = 0x0000000000000000  r15 = 0x0000000000000000  
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV boolector.c:4078 in generate_fun_model_str
==14432==ABORTING
Abort trap: 6

I'm using lingeling only.

[mpreiner]

Pushed cad16b1 to master. Let me know if this fixes your problem.

[mikhailramalho]

I'm not sure it's the same issue, but Boolector keeps crashing when I try to verify a formula with const_array.

This is a reduced trace; it crashes when trying to dump the const_array node right after creating it:
btor.trace.txt

It happens with the latest release and with cad16b1. When I try it with a debug version, it fails the following assertion:

$ ~/tools/boolector/build/bin/btoruntrace -s btor.trace 
btoruntrace: /home/mgadelha/tools/boolector/src/dumper/btordumpsmt.c:602: expand_lambda: Assertion `static_rho' failed.
Aborted (core dumped)

I'm using lingeling only.

[mpreiner]

@mikhailramalho Yeah, that's a different issue. I created a new issue for this. Let's continue the discussion there.

[dbueno]

Pushed cad16b1 to master. Let me know if this fixes your problem.

Yes, this fixes it! Thanks.