From 531d846a72d3cbb571fd37844993b67f30332bf9 Mon Sep 17 00:00:00 2001 From: Stefan Muenzel Date: Sat, 21 Oct 2023 14:59:00 +0800 Subject: [PATCH] Fix links for papers in README.md --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 4782722..303857f 100644 --- a/README.md +++ b/README.md @@ -31,9 +31,9 @@ Most of these solvers are implemented in C or C++. In contract, MC² is based on the **mcSAT** calculus (see -[[fmcad'13]](http://csl.sri.com/~dejan/papers/jovanovic-fmcad2013.pdf) +[[fmcad'13]](https://leodemoura.github.io/files/fmcad2013.pdf) and -[[vmcai'13]](http://www.csl.sri.com/users/dejan/papers/mcsat-vmcai2013.pdf)). +[[vmcai'13]](http://leodemoura.github.io/files/mcsat.pdf)). mcSAT is fundamentally different from CDCL(T); it is a so-called _natural SMT_ calculus where the boolean reasoning of CDCL is extended so as to be able to assign values to non-boolean variables (such as