Skip to content

Commit aa6fdbf

Browse files
Remove obsolete references to SMT1
1 parent 55499d9 commit aa6fdbf

File tree

3 files changed

+4
-13
lines changed

3 files changed

+4
-13
lines changed

doc/slides/cprover-overview-latex-beamer/cprover-overview-slides.tex

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -105,8 +105,7 @@
105105
\node[rectangle,fill=tachameleon!25!white] (solvers) [right of=engine4,xshift=2cm,yshift=-0.5cm]
106106
{\begin{tikzpicture}[node distance=0.75cm]
107107
\node[rectangle,fill=tachameleon!50!white] (sat) { SAT };
108-
\node[rectangle,fill=tachameleon!50!white] (smt1) [below of=sat] { SMT1 };
109-
\node[rectangle,fill=tachameleon!50!white] (smt2) [below of=smt1] { SMT2 };
108+
\node[rectangle,fill=tachameleon!50!white] (smt2) [below of=sat] { SMT2 };
110109
\node (decproc) [below of=smt2] { \tiny decision procedure };
111110
\end{tikzpicture}};
112111

scripts/vpath-setup.sh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ perl -p -i -e 's/^(irep_ids.cpp:)/#$1/' $DEST/src/util/Makefile
6060
# create sub-directories
6161
mkdir -p $DEST/src/ansi-c/library $DEST/src/ansi-c/literals
6262
mkdir -p $DEST/src/goto-instrument/{accelerate,wmm}
63-
mkdir -p $DEST/src/solvers/{flattening,floatbv,miniBDD,prop,qbf,refinement,sat,smt1,smt2}
63+
mkdir -p $DEST/src/solvers/{flattening,floatbv,miniBDD,prop,qbf,refinement,sat,smt2}
6464

6565
# copy generated files for coverage reports
6666
for f in \

src/solvers/README.md

Lines changed: 2 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -35,16 +35,8 @@ different decision procedures, roughly one per directory.
3535
post-processing function that adds extra constraints. This is not used
3636
by the SMT2 back-ends.
3737

38-
* dplib/: Provides the `dplib_dect` object which used the decision
39-
procedure library from “Decision Procedures : An Algorithmic Point of
40-
View”.
41-
42-
* smt1/: Provides the `smt1_dect` type which converts the formulae to
43-
SMTLib version 1 and then invokes one of Boolector, CVC3, OpenSMT,
44-
Yices, MathSAT or Z3. Again, note that this format is depreciated.
45-
46-
* smt2/: Provides the `smt2_dect` type which functions in a similar
47-
way to `smt1_dect`, calling Boolector, CVC3, MathSAT, Yices or Z3.
38+
* smt2/: Provides the `smt2_dect` type which converts the formulae to
39+
SMTLib 2 and then invokes one of Boolector, CVC3, CVC4, MathSAT, Yices or Z3.
4840
Note that the interaction with the solver is batched and uses
4941
temporary files rather than using the interactive command supported by
5042
SMTLib 2. With the `–fpa` option, this output mode will not flatten

0 commit comments

Comments
 (0)