Fix regressions in regress1 after #4613. (#4616)

[cvc5.git] / examples / SimpleVC.rb

diff --git a/examples/SimpleVC.rb b/examples/SimpleVC.rb
index 36af3c21564732b6bc5ab52d18f1828c2682fb2a..4f289d34f95ef1846f4f473dabe014b47e9f735e 100755 (executable)
--- a/examples/SimpleVC.rb
+++ b/examples/SimpleVC.rb
@@ -47,11 +47,11 @@ twox_plus_y = em.mkExpr(PLUS, twox, y)
 three = em.mkConst(CVC4::Integer.new(3))
 twox_plus_y_geq_3 = em.mkExpr(GEQ, twox_plus_y, three)
 
-formula = BoolExpr.new(em.mkExpr(AND, x_positive, y_positive)).impExpr(BoolExpr.new(twox_plus_y_geq_3))
+formula = Expr.new(em.mkExpr(AND, x_positive, y_positive)).impExpr(Expr.new(twox_plus_y_geq_3))
 
-puts "Checking validity of formula " + formula.toString + " with CVC4."
-puts "CVC4 should report VALID."
-puts "Result from CVC4 is: " + smt.query(formula).toString
+puts "Checking entailment of formula " + formula.toString + " with CVC4."
+puts "CVC4 should report ENTAILED."
+puts "Result from CVC4 is: " + smt.checkEntailed(formula).toString
 
 exit