projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4683179) | patch
Fixes and additions for LFSC signatures (#8120)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 21 Feb 2022 18:13:54 +0000 (12:13 -0600)
committerGitHub <noreply@github.com>
Mon, 21 Feb 2022 18:13:54 +0000 (18:13 +0000)
commit3dd30794611fa1e4344b0f7f3068211533b48f4f
tree9ba31f1d81c7633343114cc4d3f65ddedca42fe0tree
parent4683179f4aff1a1b3e797cea23f8f06ed121a406commit | diff
Fixes and additions for LFSC signatures (#8120)

Fixes a critical issue in the re intersection rule, where a null terminator was missed.

Also adds a sketch of the theory signature for floating points.
proofs/lfsc/signatures/strings_rules.plf diff | blob | history
proofs/lfsc/signatures/theory_def.plf diff | blob | history