ftsrg / theta

Generic, modular and configurable formal verification framework supporting various formalisms and algorithms
http://theta.inf.mit.bme.hu/
Apache License 2.0
49 stars 43 forks source link

XSTS Cli fixes #294

Closed mondokm closed 3 months ago

mondokm commented 3 months ago

This PR adds a different default solver for CHC and fixes cex length printing in XSTS Cli

github-actions[bot] commented 3 months ago

Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all):

task set BOUNDED CEGAR HORN
ConcurrencySafety-Main :question: (0 / 0 / 50) HTML/CSV :white_check_mark: (20 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ConcurrencySafety-MemSafety :question: (0 / 0 / 50) HTML/CSV :white_check_mark: (43 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ConcurrencySafety-NoOverflows :question: (0 / 0 / 50) HTML/CSV :white_check_mark: (39 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
NoDataRace-Main :question: (0 / 0 / 50) HTML/CSV :white_check_mark: (26 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ReachSafety-Arrays :question: (0 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ReachSafety-BitVectors :white_check_mark: (14 / 0 / 46) HTML/CSV :white_check_mark: (13 / 0 / 46) HTML/CSV :white_check_mark: (12 / 0 / 46) HTML/CSV
ReachSafety-Combinations :question: (0 / 0 / 50) HTML/CSV :white_check_mark: (3 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ReachSafety-ControlFlow :white_check_mark: (3 / 0 / 50) HTML/CSV :white_check_mark: (2 / 0 / 50) HTML/CSV :white_check_mark: (17 / 0 / 50) HTML/CSV
ReachSafety-ECA :question: (0 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ReachSafety-Floats :exclamation: (7 / 1 / 50) HTML/CSV :white_check_mark: (15 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ReachSafety-Hardware :white_check_mark: (2 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ReachSafety-Heap :white_check_mark: (2 / 0 / 11) HTML/CSV :white_check_mark: (10 / 0 / 11) HTML/CSV :exclamation: (2 / 1 / 11) HTML/CSV
ReachSafety-Loops :white_check_mark: (16 / 0 / 50) HTML/CSV :white_check_mark: (11 / 0 / 50) HTML/CSV :white_check_mark: (12 / 0 / 50) HTML/CSV
ReachSafety-Recursive :question: (0 / 0 / 50) HTML/CSV :white_check_mark: (13 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV
ReachSafety-Sequentialized :question: (0 / 0 / 50) HTML/CSV :white_check_mark: (1 / 0 / 50) HTML/CSV :white_check_mark: (2 / 0 / 50) HTML/CSV
ReachSafety-XCSP :question: (0 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV :question: (0 / 0 / 50) HTML/CSV