ostrich
ostrich copied to clipboard
uuverifiers
An SMT Solver for string constraints
Added some new flags to enable different propagation strategies for forward and backwards propagation.
Hello, I ran the following command, `./ostrich tests/case-insensitive-2.smt2` but I got an unexpected result. Why? `(error "ecma2020regex/Absyn/ControlLettera")` Did I do something wrong?
Variables without constraints do not generate model. Like the example below, the model of `len_x` and `y` will not be generated: ```sh ; sat (declare-fun x ()String) (declare-fun y ()String)...
Hi, for the following formula ostrich 2b3eb9b ~~~~ (set-logic QF_LIA) (declare-fun x () Int) (assert (> x 7)) (assert (= (mod x (- 5)) 2)) (check-sat) (get-model) (get-value (x (mod...
Hi, for the following formula ostrich 2b3eb9b ~~~~ (set-logic LRA) (declare-fun x () Real) (assert (forall ((y Real)) (=> (> y 0) (>= y x)))) (check-sat) (set-option :regular-output-channel "/dev/null") (get-model)...
Hi, for the following formula ostrich 2b3eb9b ~~~~ (set-logic QF_LRA) (check-sat) (pop 1) ~~~~ ~~~~ sat error java.lang.RuntimeException: Stack empty at scala.sys.package$.error(package.scala:27) at scala.collection.mutable.ArrayStack.pop(ArrayStack.scala:118) at ap.SimpleAPI.popHelp(SimpleAPI.scala:4008) at ap.SimpleAPI.pop(SimpleAPI.scala:3993) at ap.parser.SMTParser2InputAbsy.pop(SMTParser2InputAbsy.scala:875)...
Hi, for the following instance, ostrich https://github.com/uuverifiers/ostrich/commit/2b3eb9bf8f2323534f6c7fe10f17ab43ef7fd4da yields `unsat`, but z3 and cvc4 return `sat` ~~~~ (declare-const v0 Bool) (declare-const i1 Int) (declare-const i4 Int) (declare-const i5 Int) (declare-const r0...
Hi, for the following instance ~~~~ (set-logic NIA) (declare-const v0 Bool) (declare-const v1 Bool) (declare-const v2 Bool) (declare-const v3 Bool) (declare-const v4 Bool) (declare-const v5 Bool) (declare-const v6 Bool) (declare-const...