Skip to content

Commit

Permalink
Fixes to CI
Browse files Browse the repository at this point in the history
- Disable CARGO_INCREMENTAL for faster builds
- Change: `apt` to `apt-get`
  Removes: `WARNING: apt does not have a stable CLI interface. Use with caution in scripts.`

- Change: `continue-on-error` to `if:${{ success() || failure() }}`
          Failing builds will now get a red check mark

- Fix test_goal_apply_tactic to pass

- Disable test_solver_unknown until Z3Prover/z3#5702 is fixed
  • Loading branch information
SeeSpring committed Dec 9, 2021
1 parent ef6ca05 commit 984aa46
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 4 deletions.
9 changes: 6 additions & 3 deletions .github/workflows/rust.yml
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,9 @@ on:
pull_request:
branches: [ master ]

env:
CARGO_INCREMENTAL: 0

jobs:
build:
runs-on: ubuntu-latest
Expand All @@ -19,15 +22,15 @@ jobs:
# `Z3_mk_pbeq`, leading to linker errors. Just ignore this, I guess, until
# we figure out how to work around it. At least we have the
# statically-linked Z3 tests below...
continue-on-error: true
if: ${{ success() || failure() }}
- name: Run tests
run: cargo test -vv --all
# See above.
continue-on-error: true
if: ${{ success() || failure() }}
- name: Run tests with `arbitrary-size-numeral` enabled
run: cargo test --manifest-path z3/Cargo.toml -vv --features arbitrary-size-numeral
# See above.
continue-on-error: true
if: ${{ success() || failure() }}

build_z3_statically:
strategy:
Expand Down
3 changes: 2 additions & 1 deletion z3/tests/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -580,6 +580,7 @@ fn test_rec_func_def_unsat() {
}

#[test]
#[ignore = "See https://github.com/Z3Prover/z3/issues/5702"]
fn test_solver_unknown() {
let _ = env_logger::try_init();
let mut cfg = Config::new();
Expand Down Expand Up @@ -1251,7 +1252,7 @@ fn test_goal_apply_tactic() {
vec![a.clone(), b.clone()],
);

let a_implies_b = ast::Bool::implies(&a, &b);
let a_implies_b = ast::Bool::implies(&a, &b).simplify();
let a_and_a_implies_b = Bool::and(&ctx, &[&a, &a_implies_b]);

let goal = Goal::new(&ctx, false, false, false);
Expand Down

0 comments on commit 984aa46

Please # to comment.