| .. |
|
BMC.cpp
|
Symbolic state
|
2020-04-06 12:27:53 +02:00 |
|
BMC.h
|
Move VerificationTarget and add BMCVerificationTarget
|
2020-02-12 11:47:58 -03:00 |
|
CHC.cpp
|
[SMTChecker] Fix ICE in CHC internal calls
|
2020-04-07 01:09:03 +02:00 |
|
CHC.h
|
Add support to internal function calls
|
2020-03-11 16:29:07 +01:00 |
|
CHCSmtLib2Interface.cpp
|
Library libdevcore renamed to libsolutil.
|
2020-01-07 15:51:50 +01:00 |
|
CHCSmtLib2Interface.h
|
C++ namespace cleanup (except tests).
|
2020-01-07 15:51:50 +01:00 |
|
CHCSolverInterface.h
|
C++ namespace cleanup (except tests).
|
2020-01-07 15:51:50 +01:00 |
|
CVC4Interface.cpp
|
Library libdevcore renamed to libsolutil.
|
2020-01-07 15:51:50 +01:00 |
|
CVC4Interface.h
|
C++ namespace cleanup (except tests).
|
2020-01-07 15:51:50 +01:00 |
|
EncodingContext.cpp
|
Symbolic state
|
2020-04-06 12:27:53 +02:00 |
|
EncodingContext.h
|
Symbolic state
|
2020-04-06 12:27:53 +02:00 |
|
ModelChecker.cpp
|
Change CHC encoding to functions forest instead of explicit CFG
|
2020-03-03 12:12:26 +01:00 |
|
ModelChecker.h
|
Change CHC encoding to functions forest instead of explicit CFG
|
2020-03-03 12:12:26 +01:00 |
|
SMTEncoder.cpp
|
Symbolic state
|
2020-04-06 12:27:53 +02:00 |
|
SMTEncoder.h
|
CHC clears indices so that initial is 0 and current is 1
|
2020-02-12 11:47:58 -03:00 |
|
SMTLib2Interface.cpp
|
Library libdevcore renamed to libsolutil.
|
2020-01-07 15:51:50 +01:00 |
|
SMTLib2Interface.h
|
Library libdevcore renamed to libsolutil.
|
2020-01-07 15:51:50 +01:00 |
|
SMTPortfolio.cpp
|
Replace void cast by maybe_unused
|
2020-01-09 13:41:30 +01:00 |
|
SMTPortfolio.h
|
Library libdevcore renamed to libsolutil.
|
2020-01-07 15:51:50 +01:00 |
|
SolverInterface.h
|
[SMTChecker] Add SortProvider
|
2020-03-26 14:55:54 +01:00 |
|
Sorts.cpp
|
[SMTChecker] Add SortProvider
|
2020-03-26 14:55:54 +01:00 |
|
Sorts.h
|
[SMTChecker] Add SortProvider
|
2020-03-26 14:55:54 +01:00 |
|
SSAVariable.cpp
|
C++ namespace cleanup (except tests).
|
2020-01-07 15:51:50 +01:00 |
|
SSAVariable.h
|
C++ namespace cleanup (except tests).
|
2020-01-07 15:51:50 +01:00 |
|
SymbolicState.cpp
|
Symbolic state
|
2020-04-06 12:27:53 +02:00 |
|
SymbolicState.h
|
Symbolic state
|
2020-04-06 12:27:53 +02:00 |
|
SymbolicTypes.cpp
|
[SMTChecker] Add SortProvider
|
2020-03-26 14:55:54 +01:00 |
|
SymbolicTypes.h
|
C++ namespace cleanup (except tests).
|
2020-01-07 15:51:50 +01:00 |
|
SymbolicVariables.cpp
|
Allow constructing symbolic arrays from smt sort
|
2020-04-06 10:50:00 +02:00 |
|
SymbolicVariables.h
|
Allow constructing symbolic arrays from smt sort
|
2020-04-06 10:50:00 +02:00 |
|
VariableUsage.cpp
|
C++ namespace cleanup (except tests).
|
2020-01-07 15:51:50 +01:00 |
|
VariableUsage.h
|
C++ namespace cleanup (except tests).
|
2020-01-07 15:51:50 +01:00 |
|
Z3CHCInterface.cpp
|
Library libdevcore renamed to libsolutil.
|
2020-01-07 15:51:50 +01:00 |
|
Z3CHCInterface.h
|
C++ namespace cleanup (except tests).
|
2020-01-07 15:51:50 +01:00 |
|
Z3Interface.cpp
|
Library libdevcore renamed to libsolutil.
|
2020-01-07 15:51:50 +01:00 |
|
Z3Interface.h
|
Change CHC encoding to functions forest instead of explicit CFG
|
2020-03-03 12:12:26 +01:00 |
