(horn) Segementation fault on QF_S formula

[muchang]

Hi,
For this case, Z3 throws out a segmentation fault:

[576] % z3debug small.smt2
Segmentation fault
[577] % z3release small.smt2
Segmentation fault
[578] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==11048==ERROR: AddressSanitizer: SEGV on unknown address 0x6250000b2440 (pc 0x6250000b2440 bp 0x7ffc80258b30 sp 0x7ffc80258ac8 T0)
==11048==The signal is caused by a READ memory access.
  #0 0x6250000b243f (<unknown module>)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV (<unknown module>) 
==11048==ABORTING
[579] % 
[579] % cat small.smt2
(assert (str.in.re "ab" (re.union (re.inter (str.to.re "") (str.to.re "a")) (str.to.re "ab"))))
(check-sat-using (then horn default))

OS: Ubuntu 18.04
Commit: becf423

[muchang]

Here is another segmentation fault with assertion violation might be related to this issue:

[609] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 3197
new_fact == lit
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[610] % z3release small.smt2
Segmentation fault
[611] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==5305==ERROR: AddressSanitizer: SEGV on unknown address 0x6250000b24b0 (pc 0x6250000b24b0 bp 0x7ffc59ff6880 sp 0x7ffc59ff6818 T0)
==5305==The signal is caused by a READ memory access.
  #0 0x6250000b24af (<unknown module>)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV (<unknown module>) 
==5305==ABORTING
[612] % 
[612] % cat small.smt2
(assert (str.in.re "ab" (re.union (re.inter (str.to.re "a") (str.to.re "b")) (re.opt (str.to.re "ab")))))
(check-sat-using (then horn default))
[613] %

[NikolajBjorner]

it is too far fetched a scenario to be worth digging into at this time

[zhendongsu]

Hi Nikolaj, I'm curious to know in what ways it is a far fetched scenario. If we replace the occurrences of "ab" with for example "a", z3 returns the expected answer sat in both instances. Thanks.

This is not to argue that it shouldn't be far fetched, but an attempt to understand the yardsticks that you use to help avoid reporting such similar issues.

BTW, CVC4 provided some quite helpful guidelines for fuzzing: https://github.com/CVC4/CVC4/wiki/Fuzzing-CVC4. If possible, it would be nice to document something similar to know what are in scope and what are typically not. Such a document would be quite valuable; thanks.

[NikolajBjorner]

• it is way outside scope of Horn solver scenarios.

[zhendongsu]

• it is way outside scope of Horn solver scenarios.

Nikolaj, thanks, but then default will kick in right after horn to deal with whatever subgoals it produces, correct (which is why we get the correct sat if "ab" is replaced by "a")? The tests do also segfault the release build (not only the debug build), which is perhaps not desirable, yes?