9 files changed, 27 insertions, 27 deletions
diff --git a/examples/smtbmc/glift/C7552.ys b/examples/smtbmc/glift/C7552.ys
index 139b0df43..c1fdf244e 100644
--- a/examples/smtbmc/glift/C7552.ys
+++ b/examples/smtbmc/glift/C7552.ys
@@ -2,7 +2,7 @@ read_verilog C7552.v
 techmap
 flatten
 select C7552_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename C7552_lev2 uut
@@ -12,7 +12,7 @@ read_verilog C7552.v
 techmap
 flatten
 select C7552_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename C7552_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 techmap
 opt
 stat
-qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution C7552.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution C7552.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat
 
diff --git a/examples/smtbmc/glift/C880.ys b/examples/smtbmc/glift/C880.ys
index 93f929c89..9a5e7bdcd 100644
--- a/examples/smtbmc/glift/C880.ys
+++ b/examples/smtbmc/glift/C880.ys
@@ -2,7 +2,7 @@ read_verilog C880.v
 techmap
 flatten
 select C880_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename C880_lev2 uut
@@ -12,7 +12,7 @@ read_verilog C880.v
 techmap
 flatten
 select C880_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename C880_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 techmap
 opt
 stat
-qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution C880.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution C880.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat
 
diff --git a/examples/smtbmc/glift/alu2.ys b/examples/smtbmc/glift/alu2.ys
index 72cdaceba..f79c33ca5 100644
--- a/examples/smtbmc/glift/alu2.ys
+++ b/examples/smtbmc/glift/alu2.ys
@@ -2,7 +2,7 @@ read_verilog alu2.v
 techmap
 flatten
 select alu2_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename alu2_lev2 uut
@@ -12,7 +12,7 @@ read_verilog alu2.v
 techmap
 flatten
 select alu2_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename alu2_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 techmap
 opt
 stat
-qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution alu2.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution alu2.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat
 
diff --git a/examples/smtbmc/glift/alu4.ys b/examples/smtbmc/glift/alu4.ys
index b4337e699..3fc2112d6 100644
--- a/examples/smtbmc/glift/alu4.ys
+++ b/examples/smtbmc/glift/alu4.ys
@@ -2,7 +2,7 @@ read_verilog alu4.v
 techmap
 flatten
 select alu4_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename alu4_lev2 uut
@@ -12,7 +12,7 @@ read_verilog alu4.v
 techmap
 flatten
 select alu4_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename alu4_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 techmap
 opt
 stat
-qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution alu4.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution alu4.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat
 
diff --git a/examples/smtbmc/glift/mux2.ys b/examples/smtbmc/glift/mux2.ys
index c6670d741..a8e99912b 100644
--- a/examples/smtbmc/glift/mux2.ys
+++ b/examples/smtbmc/glift/mux2.ys
@@ -22,9 +22,9 @@ copy mux2 spec
 copy mux2 uut
 copy mux2 solved
 delete mux2
-glift -create-precise spec
-glift -create-sketch uut
-glift -create-sketch -no-cost-model solved
+glift -create-precise-model spec
+glift -create-instrumented-model uut
+glift -create-instrumented-model -no-cost-model solved
 design -push-copy
 miter -equiv spec uut qbfmiter
 flatten
diff --git a/examples/smtbmc/glift/t481.ys b/examples/smtbmc/glift/t481.ys
index 249a9eb71..282e723af 100644
--- a/examples/smtbmc/glift/t481.ys
+++ b/examples/smtbmc/glift/t481.ys
@@ -2,7 +2,7 @@ read_verilog t481.v
 techmap
 flatten
 select t481_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename t481_lev2 uut
@@ -12,7 +12,7 @@ read_verilog t481.v
 techmap
 flatten
 select t481_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename t481_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 techmap
 opt
 stat
-qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution t481.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution t481.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat
 
diff --git a/examples/smtbmc/glift/too_large.ys b/examples/smtbmc/glift/too_large.ys
index 2bb6105ea..05b9fa5dc 100644
--- a/examples/smtbmc/glift/too_large.ys
+++ b/examples/smtbmc/glift/too_large.ys
@@ -2,7 +2,7 @@ read_verilog too_large.v
 techmap
 flatten
 select too_large_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename too_large_lev2 uut
@@ -12,7 +12,7 @@ read_verilog too_large.v
 techmap
 flatten
 select too_large_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename too_large_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 techmap
 opt
 stat
-qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution too_large.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution too_large.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat
 
diff --git a/examples/smtbmc/glift/ttt2.ys b/examples/smtbmc/glift/ttt2.ys
index 62054a86c..beba8b102 100644
--- a/examples/smtbmc/glift/ttt2.ys
+++ b/examples/smtbmc/glift/ttt2.ys
@@ -2,7 +2,7 @@ read_verilog ttt2.v
 techmap
 flatten
 select ttt2_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename ttt2_lev2 uut
@@ -12,7 +12,7 @@ read_verilog ttt2.v
 techmap
 flatten
 select ttt2_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename ttt2_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 techmap
 opt
 stat
-qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution ttt2.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution ttt2.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat
 
diff --git a/examples/smtbmc/glift/x1.ys b/examples/smtbmc/glift/x1.ys
index b010fe9ee..e48a4e6ce 100644
--- a/examples/smtbmc/glift/x1.ys
+++ b/examples/smtbmc/glift/x1.ys
@@ -2,7 +2,7 @@ read_verilog x1.v
 techmap
 flatten
 select x1_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename x1_lev2 uut
@@ -12,7 +12,7 @@ read_verilog x1.v
 techmap
 flatten
 select x1_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename x1_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 techmap
 opt
 stat
-qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution x1.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution x1.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat