summaryrefslogtreecommitdiff
path: root/src/smtlib.ml
AgeCommit message (Expand)Author
2019-11-07Backport fixes to SMT generation from poly_mapping branchAlasdair Armstrong
2019-10-31Allow sail to be scripted using sailAlasdair
2019-05-21SMT: Use a separate constructor for memory read variablesAlasdair Armstrong
2019-05-21SMT: Add control flow node numbers to memory events to track program orderAlasdair Armstrong
2019-05-17SMT: Finish adding all memory builtins from lib/regfp.sailAlasdair Armstrong
2019-05-16SMT: Improve simplification for generated SMTAlasdair Armstrong
2019-05-14SMT: Allow printing SMT with an optional variable prefixAlasdair Armstrong
2019-05-10SMT: Implement memory events for read_mem and write_memAlasdair
2019-05-10SMT: Experiment with symbolic memory reads and writesAlasdair Armstrong
2019-05-10SMT: Lazily compute efficient path conditionalsAlasdair
2019-05-08SMT: Add reals and strings to SMT backendAlasdair Armstrong
2019-05-07Move parser combinators shared by property and model parsing to separate fileAlasdair Armstrong
2019-05-01Jib: Refactor V_callAlasdair Armstrong
2019-04-30SMT: Allow custom queriesAlasdair Armstrong
2019-04-29SMT: Refactor overflow checks into generic event checking systemAlasdair Armstrong
2019-04-27Merge branch 'sail2' into smt_experimentsAlasdair
2019-04-24SMT: Can now recheck some simple models via the interpreterAlasdair
2019-04-23SMT: Add parser for generated modelsAlasdair Armstrong
2019-04-16SMT: Fix inlining issuesAlasdair Armstrong
2019-04-16SMT: Add struct value literalsAlasdair
2019-04-13SMT: More builtinsAlasdair
2019-04-10SMT: Add some simple constant folding for generated SMTAlasdair
2019-04-09SMT: Experimental Jib->SMT translationAlasdair Armstrong