rainoftime

Parse errors

2

It seems sally can only parse examples from `/test/regess/*`. Whenever running the mcmt cases from the `examples` folder, I got the following information: `Parse error: ../../examples/honeywell/Ex3.mcmt:28:20: ` And the sal...

C++ API for sally?

1

Hi, is there any plan for providing C++ api for creating and verifying a transition system?

[Consolidated] Issues related to qe_rec

4

**Assertion error at src/qe/qe_mbp.cpp:275** Hi, for the following formula z3 5da71dc847 ~~~~ (set-logic NIA) (declare-fun i1 () Int) (set-option :rewriter.mul_to_power true) (set-option :rewriter.blast_distinct true) (set-option :rewriter.eq2ineq true) (declare-fun i6 ()...

Displaying solving results when using --dimacs on trivial sat/unsat formulas

1

Hi, I tried running `yices-smt2 --dimacs=tmp.cnf test.smt2` on the following trivial formula ~~~~ (set-logic QF_BV) (declare-fun x () (_ BitVec 16)) (assert (= x (_ bv1 16))) (assert (= x...

Support string-typed parameters

1

I notice that we can set boolean or integer typed parameters to a tactic such as `simplify'. Can we specify a parameter whose type is string? Thank you! ~~~~ "simplify":...